1 /-
2 Copyright (c) 2018 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Mario Carneiro
5 -/
6
7 import algebra.big_operators algebra.ordered_field
src └───────────────────┘ └───────────────────┘
8
9 /-!
10 # Cauchy sequences
11
12 A basic theory of Cauchy sequences, used in the construction of the reals and p-adic numbers. Where
13 applicable, lemmas that will be reused in other contexts have been stated in extra generality.
14
15 There are other "versions" of Cauchyness in the library, in particular Cauchy filters in topology.
16 This is a concrete implementation that is useful for simplicity and computability reasons.
17
18 ## Important definitions
19
20 * `is_absolute_value`: a type class stating that `f : β → α` satisfies the axioms of an abs val
21 * `is_cau_seq`: a predicate that says `f : ℕ → β` is Cauchy.
22
23 ## Tags
24
25 sequence, cauchy, abs val, absolute value
26 -/
27
28 /-- A function f is an absolute value if it is nonnegative, zero only at 0, additive, and
29 multiplicative. -/
30 class is_absolute_value {α} [discrete_linear_ordered_field α]
id ┴ └───────────────────────────┘ ┴
src └───────────────────────────┘
typ ┴ └───────────────────────────┘ ┴
31 {β} [ring β] (f : β → α) : Prop :=
id ┴ └──┘ ┴ ┴ ┴ ┴
src └──┘
typ ┴ └──┘ ┴ ┴ ┴ ┴
32 (abv_nonneg : ∀ x, 0 ≤ f x)
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
33 (abv_eq_zero : ∀ {x}, f x = 0 ↔ x = 0)
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
34 (abv_add : ∀ x y, f (x + y) ≤ f x + f y)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
35 (abv_mul : ∀ x y, f (x * y) = f x * f y)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
36
37 namespace is_absolute_value
38 variables {α : Type*} [discrete_linear_ordered_field α]
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
39 {β : Type*} [ring β] (abv : β → α) [is_absolute_value abv]
id └──┘ └───────────────┘
src └──┘ └───────────────┘
typ └──┘ └───────────────┘
doc └───────────────┘
40
41 theorem abv_zero : abv 0 = 0 := (abv_eq_zero abv).2 rfl
id └─┘ ┴ └─────────┘ └─┘ ┴ └─┘
src ┴ └─────────┘ ┴ └─┘
typ └─┘ ┴ └─────────┘ └─┘ ┴ └─┘
42
43 theorem abv_one' (h : (1:β) ≠ 0) : abv 1 = 1 :=
id ┴ ┴ └─┘ ┴
src ┴ ┴
typ ┴ ┴ └─┘ ┴
44 (domain.mul_left_inj $ mt (abv_eq_zero abv).1 h).1 $
id └─────────────────┘ └┘ └─────────┘ └─┘ ┴ ┴ ┴
src └─────────────────┘ └┘ └─────────┘ ┴ ┴
typ └─────────────────┘ └┘ └─────────┘ └─┘ ┴ ┴ ┴
doc └─────────────────┘
45 by rw [← abv_mul abv, mul_one, mul_one]
id └─────┘ └─┘ └─────┘ └─────┘
src └────┘└─────┘┴ └┘└─────┘└┘└─────┘└─
typ └────┘└─────┘┴└─┘└┘└─────┘└┘└─────┘└─
doc └────┘ ┴ └┘ └┘ └─
txt └────┘ ┴ └┘ └┘ └─
par └────┘ ┴ └┘ └┘ └─
pid └──┘ ┴ └┘ └┘ ┴└
st └────────────────┘└───────┘└───────┘┴└
46
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
47 theorem abv_one
48 {β : Type*} [domain β] (abv : β → α) [is_absolute_value abv] :
id └────┘ ┴ ┴ ┴ └───────────────┘ └─┘
src └────┘ └───────────────┘
typ └────┘ ┴ ┴ ┴ └───────────────┘ └─┘
doc └────┘ └───────────────┘
49 abv 1 = 1 := abv_one' abv one_ne_zero
id └─┘ ┴ └──────┘ └─┘ └─────────┘
src ┴ └──────┘ └─────────┘
typ └─┘ ┴ └──────┘ └─┘ └─────────┘
50
51 theorem abv_pos {a : β} : 0 < abv a ↔ a ≠ 0 :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
52 by rw [lt_iff_le_and_ne, ne, eq_comm]; simp [abv_eq_zero abv, abv_nonneg abv]
id └──────────────┘ └┘ └─────┘ └─────────┘ └─┘ └────────┘ └─┘
src └──┘└──────────────┘└┘└┘└┘└─────┘┴ └────┘└─────────┘┴ └┘└────────┘┴ └─
typ └──┘└──────────────┘└┘└┘└┘└─────┘┴ └────┘└─────────┘┴└─┘└┘└────────┘┴└─┘└─
doc └──┘ └┘ └┘ ┴ └────┘ ┴ └┘ ┴ └─
txt └──┘ └┘ └┘ ┴ └────┘ ┴ └┘ ┴ └─
par └──┘ └┘ └┘ ┴ └────┘ ┴ └┘ ┴ └─
pid └┘ └┘ └┘ ┴ ┴┴ ┴ └┘ ┴ ┴└
st └───────────────────┘└──┘└───────┘┴└────────────────────────────────────────
53
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
54 theorem abv_neg (a : β) : abv (-a) = abv a :=
id ┴ └─┘ ┴┴ ┴ └─┘ ┴
src ┴ ┴
typ ┴ └─┘ ┴┴ ┴ └─┘ ┴
55 by rw [← mul_self_inj_of_nonneg (abv_nonneg abv _) (abv_nonneg abv _),
id └────────────────────┘ └────────┘ └─┘
src └────┘└────────────────────┘┴ ┴ └──┘ └────────┘┴ └────
typ └────┘└────────────────────┘┴ ┴ └──┘ └────────┘┴└─┘└────
doc └────┘ ┴ ┴ └──┘ ┴ └────
txt └────┘ ┴ ┴ └──┘ ┴ └────
par └────┘ ┴ ┴ └──┘ ┴ └────
pid └──┘ ┴ ┴ └──┘ ┴ └────
st └─────────────────────────────────────────────────────────────────┘└─
56 ← abv_mul abv, ← abv_mul abv]; simp
id └─────┘ └─┘ └─────┘ └─┘
src ───┘└─────┘┴ └──┘└─────┘┴ ┴ └────
typ ───┘└─────┘┴└─┘└──┘└─────┘┴└─┘┴ └────
doc ───┘ ┴ └──┘ ┴ ┴ └────
txt ───┘ ┴ └──┘ ┴ ┴ └────
par ───┘ ┴ └──┘ ┴ ┴ └────
pid ───┘ ┴ └──┘ ┴ ┴ └
st ──────────────┘└─────────────┘┴└──────
57
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
58 theorem abv_sub (a b : β) : abv (a - b) = abv (b - a) :=
id ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
59 by rw [← neg_sub, abv_neg abv]
id └─────┘ └─────┘ └─┘
src └────┘└─────┘└┘└─────┘┴ └─
typ └────┘└─────┘└┘└─────┘┴└─┘└─
doc └────┘ └┘ ┴ └─
txt └────┘ └┘ ┴ └─
par └────┘ └┘ ┴ └─
pid └──┘ └┘ ┴ ┴└
st └────────────┘└───────────┘┴└
60
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
61 theorem abv_inv
62 {β : Type*} [discrete_field β] (abv : β → α) [is_absolute_value abv]
id └────────────┘ ┴ ┴ ┴ └───────────────┘ └─┘
src └────────────┘ └───────────────┘
typ └────────────┘ ┴ ┴ ┴ └───────────────┘ └─┘
doc └───────────────┘
63 (a : β) : abv a⁻¹ = (abv a)⁻¹ :=
id ┴ └─┘ ┴└┘ ┴ └─┘ ┴ └┘
src └┘ ┴ └┘
typ ┴ └─┘ ┴└┘ ┴ └─┘ ┴ └┘
64 classical.by_cases
id └────────────────┘
src └────────────────┘
typ └────────────────┘
65 (λ h : a = 0, by simp [h, abv_zero abv])
id ┴ ┴ ┴ └──────┘ └─┘
src ┴ └────┘ └┘└──────┘┴ ┴
typ ┴ ┴ └────┘┴└┘└──────┘┴└─┘┴
doc └────┘ └┘ ┴ ┴
txt └────┘ └┘ ┴ ┴
par └────┘ └┘ ┴ ┴
pid ┴┴ └┘ ┴ ┴
st └─────────────────────┘
66 (λ h, (domain.mul_left_inj (mt (abv_eq_zero abv).1 h)).1 $
id ┴ └─────────────────┘ └┘ └─────────┘ └─┘ ┴ ┴ ┴
src └─────────────────┘ └┘ └─────────┘ ┴ ┴
typ ┴ └─────────────────┘ └┘ └─────────┘ └─┘ ┴ ┴ ┴
doc └─────────────────┘
67 by rw [← abv_mul abv]; simp [h, mt (abv_eq_zero abv).1 h, abv_one abv])
id └─────┘ └─┘ ┴ └┘ └─────────┘ └─┘ ┴ └─────┘ └─┘
src └────┘└─────┘┴ ┴ └────┘ └┘└┘┴ └─────────┘┴ └──┘ └┘└─────┘┴ ┴
typ └────┘└─────┘┴└─┘┴ └────┘┴└┘└┘┴ └─────────┘┴└─┘└──┘┴└┘└─────┘┴└─┘┴
doc └────┘ ┴ ┴ └────┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴
txt └────┘ ┴ ┴ └────┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴
par └────┘ ┴ ┴ └────┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴
pid └──┘ ┴ ┴ ┴┴ └┘ ┴ ┴ └──┘ └┘ ┴ ┴
st └────────────────┘┴└───────────────────────────────────────────────┘
68
69 theorem abv_div
70 {β : Type*} [discrete_field β] (abv : β → α) [is_absolute_value abv]
id └────────────┘ ┴ ┴ ┴ └───────────────┘ └─┘
src └────────────┘ └───────────────┘
typ └────────────┘ ┴ ┴ ┴ └───────────────┘ └─┘
doc └───────────────┘
71 (a b : β) : abv (a / b) = abv a / abv b :=
id ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
72 by rw [division_def, abv_mul abv, abv_inv abv]; refl
id └──────────┘ └─────┘ └─┘ └─────┘ └─┘
src └──┘└──────────┘└┘└─────┘┴ └┘└─────┘┴ ┴ └────
typ └──┘└──────────┘└┘└─────┘┴└─┘└┘└─────┘┴└─┘┴ └────
doc └──┘ └┘ ┴ └┘ ┴ ┴ └────
txt └──┘ └┘ ┴ └┘ ┴ ┴ └────
par └──┘ └┘ ┴ └┘ ┴ ┴ └────
pid └┘ └┘ ┴ └┘ ┴ ┴ └
st └───────────────┘└───────────┘└───────────┘┴└──────
73
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
74 lemma abv_sub_le (a b c : β) : abv (a - c) ≤ abv (a - b) + abv (b - c) :=
id ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
75 by simpa using abv_add abv (a - b) (b - c)
id └─────┘ └─┘ ┴ ┴ ┴ ┴
src └──────────┘└─────┘┴ ┴ ┴┴┴ └┘ ┴ ┴ └─
typ └──────────┘└─────┘┴└─┘┴ ┴┴┴┴ └┘ ┴┴ ┴┴└─
doc └──────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─
txt └──────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─
par └──────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─
pid ┴└────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└
st └────────────────────────────────────────
76
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
77 lemma sub_abv_le_abv_sub (a b : β) : abv a - abv b ≤ abv (a - b) :=
id ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
78 sub_le_iff_le_add.2 $ by simpa using abv_add abv (a - b) b
id └───────────────┘┴ └─────┘ └─┘ ┴ ┴ ┴
src └───────────────┘┴ └──────────┘└─────┘┴ ┴ ┴┴┴ └┘ └
typ └───────────────┘┴ └──────────┘└─────┘┴└─┘┴ ┴┴┴┴ └┘┴└
doc └──────────┘ ┴ ┴ ┴ ┴ └┘ └
txt └──────────┘ ┴ ┴ ┴ ┴ └┘ └
par └──────────┘ ┴ ┴ ┴ ┴ └┘ └
pid ┴└────┘ ┴ ┴ ┴ ┴ └┘ └
st └──────────────────────────────────
79
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
80 lemma abs_abv_sub_le_abv_sub (a b : β) :
id ┴
typ ┴
81 abs (abv a - abv b) ≤ abv (a - b) :=
id └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ └─┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
82 abs_sub_le_iff.2 ⟨sub_abv_le_abv_sub abv _ _,
id └────────────┘┴ └────────────────┘ └─┘
src └────────────┘┴ └────────────────┘
typ └────────────┘┴ └────────────────┘ └─┘
83 by rw abv_sub abv; apply sub_abv_le_abv_sub abv⟩
id └─────┘ └─┘ └────────────────┘ └─┘
src └─┘└─────┘┴ └────┘└────────────────┘┴
typ └─┘└─────┘┴└─┘ └────┘└────────────────┘┴└─┘
doc └─┘ ┴ └────┘ ┴
txt └─┘ ┴ └────┘ ┴
par └─┘ ┴ └────┘ ┴
pid ┴ ┴ ┴ ┴
st └───────────────────────────────────────────┘
84
85 lemma abv_pow {β : Type*} [domain β] (abv : β → α) [is_absolute_value abv]
id └────┘ ┴ ┴ ┴ └───────────────┘ └─┘
src └────┘ └───────────────┘
typ └────┘ ┴ ┴ ┴ └───────────────┘ └─┘
doc └────┘ └───────────────┘
86 (a : β) (n : ℕ) : abv (a ^ n) = abv a ^ n :=
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
87 by induction n; simp [abv_mul abv, _root_.pow_succ, abv_one abv, *]
id ┴ └─────┘ └─┘ └─────────────┘ └─────┘ └─┘
src └────────┘ └────┘└─────┘┴ └┘└─────────────┘└┘└─────┘┴ └────
typ └────────┘┴ └────┘└─────┘┴└─┘└┘└─────────────┘└┘└─────┘┴└─┘└────
doc └────────┘ └────┘ ┴ └┘ └┘ ┴ └────
txt └────────┘ └────┘ ┴ └┘ └┘ ┴ └────
par └────────┘ └────┘ ┴ └┘ └┘ ┴ └────
pid ┴ ┴┴ ┴ └┘ └┘ ┴ └──┘└
st └─────────────────────────────────────────────────────────────────
88
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
89 end is_absolute_value
90
91 instance abs_is_absolute_value {α} [discrete_linear_ordered_field α] :
id └───────────────────────────┘ ┴
src └───────────────────────────┘
typ └───────────────────────────┘ ┴
92 is_absolute_value (abs : α → α) :=
id └───────────────┘ └─┘ ┴ ┴
src └───────────────┘ └─┘
typ └───────────────┘ └─┘ ┴ ┴
doc └───────────────┘
93 { abv_nonneg := abs_nonneg,
id └────────┘
src └────────┘
typ └────────┘
94 abv_eq_zero := λ _, abs_eq_zero,
id ┴ └─────────┘
src └─────────┘
typ ┴ └─────────┘
95 abv_add := abs_add,
id └─────┘
src └─────┘
typ └─────┘
96 abv_mul := abs_mul }
id └─────┘
src └─────┘
typ └─────┘
97
98 open is_absolute_value
99
100 theorem exists_forall_ge_and {α} [linear_order α] {P Q : α → Prop} :
id └──────────┘ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴
101 (∃ i, ∀ j ≥ i, P j) → (∃ i, ∀ j ≥ i, Q j) →
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
102 ∃ i, ∀ j ≥ i, P j ∧ Q j
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
103 | ⟨a, h₁⟩ ⟨b, h₂⟩ := let ⟨c, ac, bc⟩ := exists_ge_of_linear a b in
id ┴ └┘ ┴ └┘ └─┘ ┴ └┘ └┘ └─────────────────┘
src └─────────────────┘
typ ┴ └┘ ┴ └┘ └─┘ ┴ └┘ └┘ └─────────────────┘
104 ⟨c, λ j hj, ⟨h₁ _ (le_trans ac hj), h₂ _ (le_trans bc hj)⟩⟩
id ┴ └┘ └──────┘ └┘ └──────┘ └┘
src └──────┘ └──────┘
typ ┴ └┘ └──────┘ └┘ └──────┘ └┘
105
106 section
107 variables {α : Type*} [discrete_linear_ordered_field α]
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
108 {β : Type*} [ring β] (abv : β → α) [is_absolute_value abv]
id └──┘ └───────────────┘
src └──┘ └───────────────┘
typ └──┘ └───────────────┘
doc └───────────────┘
109
110 theorem rat_add_continuous_lemma
111 {ε : α} (ε0 : 0 < ε) : ∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β},
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
112 abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ + a₂ - (b₁ + b₂)) < ε :=
id └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴
113 ⟨ε / 2, half_pos ε0, λ a₁ a₂ b₁ b₂ h₁ h₂,
id ┴ ┴ └──────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
src ┴ └──────┘
typ ┴ ┴ └──────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
114 by simpa [add_halves] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add h₁ h₂)⟩
id └────────┘ └────────────┘ └─────┘ └─┘ └────────┘ └┘ └┘
src └─────┘└────────┘└──────┘└────────────┘┴ └─────┘┴ └────┘ └────────┘┴ ┴ ┴
typ └─────┘└────────┘└──────┘└────────────┘┴ └─────┘┴└─┘└────┘ └────────┘┴└┘┴└┘┴
doc └─────┘ └──────┘ ┴ ┴ └────┘ ┴ ┴ ┴
txt └─────┘ └──────┘ ┴ ┴ └────┘ ┴ ┴ ┴
par └─────┘ └──────┘ ┴ ┴ └────┘ ┴ ┴ ┴
pid ┴┴ ┴┴└────┘ ┴ ┴ └────┘ ┴ ┴ ┴
st └───────────────────────────────────────────────────────────────────────────┘
115
116 theorem rat_mul_continuous_lemma
117 {ε K₁ K₂ : α} (ε0 : 0 < ε) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
118 ∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ →
id ┴ ┴ ┴ ┴ └─┘ └┘ ┴ └┘ └─┘ └┘ ┴ └┘
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ └┘ └─┘ └┘ ┴ └┘
119 abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε :=
id └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ ┴ └─┘ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴
120 begin
st └─────
121 have K0 : (0 : α) < max 1 (max K₁ K₂) := lt_of_lt_of_le zero_lt_one (le_max_left _ _),
id ┴ ┴ └─┘ └┘ └┘ └────────────┘ └─────────┘ └─────────┘
src └────────┘ └──┘ └┘┴┴ └─┘ └─┘┴ ┴ └───┘└────────────┘┴└─────────┘┴ └─────────┘└───┘
typ └────────┘ └──┘┴└┘┴┴ └─┘ └─┘┴└┘┴└┘└───┘└────────────┘┴└─────────┘┴ └─────────┘└───┘
doc └────────┘ └──┘ └┘ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴ └───┘
txt └────────┘ └──┘ └┘ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴ └───┘
par └────────┘ └──┘ └┘ ┴ └─┘ ┴ ┴ └───┘ ┴ ┴ └───┘
pid └─────┘└─┘ └──┘ └┘ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ ┴ └───┘
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
122 have εK := div_pos (half_pos ε0) K0,
id └─────┘ └──────┘ └┘ └┘
src └─────────┘└─────┘┴ └──────┘┴ └┘
typ └─────────┘└─────┘┴ └──────┘┴└┘└┘└┘
doc └─────────┘ ┴ ┴ └┘
txt └─────────┘ ┴ ┴ └┘
par └─────────┘ ┴ ┴ └┘
pid └─────┘┴└─┘ ┴ ┴ └┘
st ────────────────────────────────────┘└─
123 refine ⟨_, εK, λ a₁ a₂ b₁ b₂ ha₁ hb₂ h₁ h₂, _⟩,
id └┘
src └─────┘ └─┘ └┘ └────────────────────────────┘
typ └─────┘ └─┘└┘└┘ └────────────────────────────┘
doc └─────┘ └─┘ └┘ └────────────────────────────┘
txt └─────┘ └─┘ └┘ └────────────────────────────┘
par └─────┘ └─┘ └┘ └────────────────────────────┘
pid ┴ └─┘ └┘ └────────────────────────────┘
st ───────────────────────────────────────────────┘└─
124 replace ha₁ := lt_of_lt_of_le ha₁ (le_trans (le_max_left _ K₂) (le_max_right 1 _)),
id └────────────┘ └─┘ └──────┘ └─────────┘ └┘ └──────────┘
src └─────────────┘└────────────┘┴ ┴ └──────┘┴ └─────────┘└─┘ └┘ └──────────┘└────┘
typ └─────────────┘└────────────┘┴└─┘┴ └──────┘┴ └─────────┘└─┘└┘└┘ └──────────┘└────┘
doc └─────────────┘ ┴ ┴ ┴ └─┘ └┘ └────┘
txt └─────────────┘ ┴ ┴ ┴ └─┘ └┘ └────┘
par └─────────────┘ ┴ ┴ ┴ └─┘ └┘ └────┘
pid └──┘┴└─┘ ┴ ┴ ┴ └─┘ └┘ └────┘
st ───────────────────────────────────────────────────────────────────────────────────┘└─
125 replace hb₂ := lt_of_lt_of_le hb₂ (le_trans (le_max_right K₁ _) (le_max_right 1 _)),
id └────────────┘ └─┘ └──────┘ └┘ └──────────┘
src └─────────────┘└────────────┘┴ ┴ └──────┘┴ ┴ └──┘ └──────────┘└────┘
typ └─────────────┘└────────────┘┴└─┘┴ └──────┘┴ ┴└┘└──┘ └──────────┘└────┘
doc └─────────────┘ ┴ ┴ ┴ ┴ └──┘ └────┘
txt └─────────────┘ ┴ ┴ ┴ ┴ └──┘ └────┘
par └─────────────┘ ┴ ┴ ┴ ┴ └──┘ └────┘
pid └──┘┴└─┘ ┴ ┴ ┴ ┴ └──┘ └────┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
126 have := add_lt_add
id └────────┘
src └──────┘└────────┘└
typ └──────┘└────────┘└
doc └──────┘ └
txt └──────┘ └
par └──────┘ └
pid └───┘└─┘ └
st ─────────────────────
127 (mul_lt_mul' (le_of_lt h₁) hb₂ (abv_nonneg abv _) εK)
id └┘ └─┘
src ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ └─
typ ───┘ ┴ ┴└┘└┘└─┘┴ ┴ └──┘ └─
doc ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ └─
txt ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ └─
par ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ └─
pid ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ └─
st ──────────────────────────────────────────────────────────
128 (mul_lt_mul' (le_of_lt h₂) ha₁ (abv_nonneg abv _) εK),
id └─────────┘ └──────┘ └┘ └─┘ └────────┘ └─┘ └┘
src ───┘ └─────────┘┴ └──────┘┴ └┘ ┴ └────────┘┴ └──┘ ┴
typ ───┘ └─────────┘┴ └──────┘┴└┘└┘└─┘┴ └────────┘┴└─┘└──┘└┘┴
doc ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ ┴
txt ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ ┴
par ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ ┴
pid ───┘ ┴ ┴ └┘ ┴ ┴ └──┘ ┴
st ────────────────────────────────────────────────────────┘└─
129 rw [← abv_mul abv, mul_comm, div_mul_cancel _ (ne_of_gt K0), ← abv_mul abv, add_halves] at this,
id └─────┘ └─┘ └──────┘ └────────────┘ └──────┘ └┘ └─────┘ └─┘ └────────┘
src └────┘└─────┘┴ └┘└──────┘└┘└────────────┘└─┘ └──────┘┴ └───┘└─────┘┴ └┘└────────┘└───────┘
typ └────┘└─────┘┴└─┘└┘└──────┘└┘└────────────┘└─┘ └──────┘┴└┘└───┘└─────┘┴└─┘└┘└────────┘└───────┘
doc └────┘ ┴ └┘ └┘ └─┘ ┴ └───┘ ┴ └┘ └───────┘
txt └────┘ ┴ └┘ └┘ └─┘ ┴ └───┘ ┴ └┘ └───────┘
par └────┘ ┴ └┘ └┘ └─┘ ┴ └───┘ ┴ └┘ └───────┘
pid └──┘ ┴ └┘ └┘ └─┘ ┴ └───┘ ┴ └┘ ┴└──────┘
st ──────────────────┘└────────┘└──────────────────────────────┘└─────────────┘└──────────┘┴└──────┘└─
130 simpa [mul_add, add_mul] using lt_of_le_of_lt (abv_add abv _ _) this
id └─────┘ └─────┘ └────────────┘ └─────┘ └─┘ └──┘
src └─────┘└─────┘└┘└─────┘└──────┘└────────────┘┴ └─────┘┴ └────┘ ┴
typ └─────┘└─────┘└┘└─────┘└──────┘└────────────┘┴ └─────┘┴└─┘└────┘└──┘┴
doc └─────┘ └┘ └──────┘ ┴ ┴ └────┘ ┴
txt └─────┘ └┘ └──────┘ ┴ ┴ └────┘ ┴
par └─────┘ └┘ └──────┘ ┴ ┴ └────┘ ┴
pid ┴┴ └┘ ┴┴└────┘ ┴ ┴ └────┘ ┴
st ──────────────────────────────────────────────────────────────────────┘
131 end
st └─┘
132
133 theorem rat_inv_continuous_lemma
134 {β : Type*} [discrete_field β] (abv : β → α) [is_absolute_value abv]
id └────────────┘ ┴ ┴ ┴ └───────────────┘ └─┘
src └────────────┘ └───────────────┘
typ └────────────┘ ┴ ┴ ┴ └───────────────┘ └─┘
doc └───────────────┘
135 {ε K : α} (ε0 : 0 < ε) (K0 : 0 < K) :
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
136 ∃ δ > 0, ∀ {a b : β}, K ≤ abv a → K ≤ abv b →
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴
137 abv (a - b) < δ → abv (a⁻¹ - b⁻¹) < ε :=
id └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└┘ ┴ ┴└┘ ┴ ┴
src ┴ ┴ └┘ ┴ └┘ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└┘ ┴ ┴└┘ ┴ ┴
138 begin
st └─────
139 have KK := mul_pos K0 K0,
id └─────┘ └┘
src └─────────┘└─────┘┴ ┴
typ └─────────┘└─────┘┴ ┴└┘
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ─────────────────────────┘└─
140 have εK := mul_pos ε0 KK,
id └─────┘ └┘ └┘
src └─────────┘└─────┘┴ ┴
typ └─────────┘└─────┘┴└┘┴└┘
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ─────────────────────────┘└─
141 refine ⟨_, εK, λ a b ha hb h, _⟩,
id └┘
src └─────┘ └─┘ └┘ └──────────────┘
typ └─────┘ └─┘└┘└┘ └──────────────┘
doc └─────┘ └─┘ └┘ └──────────────┘
txt └─────┘ └─┘ └┘ └──────────────┘
par └─────┘ └─┘ └┘ └──────────────┘
pid ┴ └─┘ └┘ └──────────────┘
st ─────────────────────────────────┘└─
142 have a0 := lt_of_lt_of_le K0 ha,
id └────────────┘ └┘ └┘
src └─────────┘└────────────┘┴ ┴
typ └─────────┘└────────────┘┴└┘┴└┘
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ────────────────────────────────┘└─
143 have b0 := lt_of_lt_of_le K0 hb,
id └────────────┘ └┘ └┘
src └─────────┘└────────────┘┴ ┴
typ └─────────┘└────────────┘┴└┘┴└┘
doc └─────────┘ ┴ ┴
txt └─────────┘ ┴ ┴
par └─────────┘ ┴ ┴
pid └─────┘┴└─┘ ┴ ┴
st ────────────────────────────────┘└─
144 rw [inv_sub_inv ((abv_pos abv).1 a0) ((abv_pos abv).1 b0),
id └─────────┘ └┘ └─────┘ └─┘ └┘
src └──┘└─────────┘┴ ┴ └──┘ └┘ └─────┘┴ └──┘ └──
typ └──┘└─────────┘┴ ┴ └──┘└┘└┘ └─────┘┴└─┘└──┘└┘└──
doc └──┘ ┴ ┴ └──┘ └┘ ┴ └──┘ └──
txt └──┘ ┴ ┴ └──┘ └┘ ┴ └──┘ └──
par └──┘ ┴ ┴ └──┘ └┘ ┴ └──┘ └──
pid └┘ ┴ ┴ └──┘ └┘ ┴ └──┘ └──
st ──────────────────────────────────────────────────────────┘└─
145 abv_div abv, abv_mul abv, mul_comm, abv_sub abv,
id └─────┘ └─┘ └─────┘ └─┘ └──────┘ └─────┘ └─┘
src ─────┘└─────┘┴ └┘└─────┘┴ └┘└──────┘└┘└─────┘┴ └─
typ ─────┘└─────┘┴└─┘└┘└─────┘┴└─┘└┘└──────┘└┘└─────┘┴└─┘└─
doc ─────┘ ┴ └┘ ┴ └┘ └┘ ┴ └─
txt ─────┘ ┴ └┘ ┴ └┘ └┘ ┴ └─
par ─────┘ ┴ └┘ ┴ └┘ └┘ ┴ └─
pid ─────┘ ┴ └┘ ┴ └┘ └┘ ┴ └─
st ────────────────┘└───────────┘└────────┘└───────────┘└─
146 ← mul_div_cancel ε (ne_of_gt KK)],
id └────────────┘ ┴ └──────┘ └┘
src ───────┘└────────────┘┴ ┴ └──────┘┴ └┘
typ ───────┘└────────────┘┴┴┴ └──────┘┴└┘└┘
doc ───────┘ ┴ ┴ ┴ └┘
txt ───────┘ ┴ ┴ ┴ └┘
par ───────┘ ┴ ┴ ┴ └┘
pid ───────┘ ┴ ┴ ┴ └┘
st ─────────────────────────────────────┘└──
147 exact div_lt_div h
id └────────┘ ┴
src └────┘└────────┘┴ └
typ └────┘└────────┘┴┴└
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴ ┴ └
st ─────────────────────
148 (mul_le_mul hb ha (le_of_lt K0) (abv_nonneg abv _))
id └────────┘ └┘ └┘ └┘ └────────┘ └─┘
src ───┘ └────────┘┴ ┴ ┴ ┴ └┘ └────────┘┴ └────
typ ───┘ └────────┘┴└┘┴└┘┴ ┴└┘└┘ └────────┘┴└─┘└────
doc ───┘ ┴ ┴ ┴ ┴ └┘ ┴ └────
txt ───┘ ┴ ┴ ┴ ┴ └┘ ┴ └────
par ───┘ ┴ ┴ ┴ ┴ └┘ ┴ └────
pid ───┘ ┴ ┴ ┴ ┴ └┘ ┴ └────
st ────────────────────────────────────────────────────────
149 (le_of_lt $ mul_pos ε0 KK) KK
id └──────┘ └─────┘ └┘ └┘
src ───┘ └──────┘┴ ┴└─────┘┴ ┴ └┘ ┴
typ ───┘ └──────┘┴ ┴└─────┘┴└┘┴ └┘└┘┴
doc ───┘ ┴ ┴ ┴ ┴ └┘ ┴
txt ───┘ ┴ ┴ ┴ ┴ └┘ ┴
par ───┘ ┴ ┴ ┴ ┴ └┘ ┴
pid ───┘ ┴ ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────┘
150 end
st └─┘
151 end
152
153 /-- A sequence is Cauchy if the distance between its entries tends to zero. -/
154 def is_cau_seq {α : Type*} [discrete_linear_ordered_field α]
id └───────────────────────────┘ ┴
src └───────────────────────────┘
typ └───────────────────────────┘ ┴
155 {β : Type*} [ring β] (abv : β → α) (f : ℕ → β) :=
id └──┘ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴
156 ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - f i) < ε
id ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
157
158 namespace is_cau_seq
159 variables {α : Type*} [discrete_linear_ordered_field α]
id └───────────────────────────┘
src └───────────────────────────┘
typ └───────────────────────────┘
160 {β : Type*} [ring β] {abv : β → α} [is_absolute_value abv] {f : ℕ → β}
id └──┘ └───────────────┘ ┴
src └──┘ └───────────────┘ ┴
typ └──┘ └───────────────┘ ┴
doc └───────────────┘
161
162 theorem cauchy₂ (hf : is_cau_seq abv f) {ε:α} (ε0 : ε > 0) :
id └────────┘ └─┘ ┴ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ └─┘ ┴ ┴ ┴ ┴
doc └────────┘
163 ∃ i, ∀ j k ≥ i, abv (f j - f k) < ε :=
id ┴ ┴┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
164 begin
st └─────
165 refine (hf _ (half_pos ε0)).imp (λ i hi j k ij ik, _),
id └┘ └──────┘ └┘
src └─────┘ └─┘ └──────┘┴ └─────┘ └─────────────────┘
typ └─────┘ └┘└─┘ └──────┘┴└┘└─────┘ └─────────────────┘
doc └─────┘ └─┘ ┴ └─────┘ └─────────────────┘
txt └─────┘ └─┘ ┴ └─────┘ └─────────────────┘
par └─────┘ └─┘ ┴ └─────┘ └─────────────────┘
pid ┴ └─┘ ┴ └─────┘ └─────────────────┘
st ──────────────────────────────────────────────────────┘└─
166 rw ← add_halves ε,
id └────────┘ ┴
src └───┘└────────┘┴
typ └───┘└────────┘┴┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ──────────────────┘└─
167 refine lt_of_le_of_lt (abv_sub_le abv _ _ _) (add_lt_add (hi _ ij) _),
id └────────────┘ └────────┘ └─┘ └────────┘ └┘ └┘
src └─────┘└────────────┘┴ └────────┘┴ └──────┘ └────────┘┴ └─┘ └──┘
typ └─────┘└────────────┘┴ └────────┘┴└─┘└──────┘ └────────┘┴ └┘└─┘└┘└──┘
doc └─────┘ ┴ ┴ └──────┘ ┴ └─┘ └──┘
txt └─────┘ ┴ ┴ └──────┘ ┴ └─┘ └──┘
par └─────┘ ┴ ┴ └──────┘ ┴ └─┘ └──┘
pid ┴ ┴ ┴ └──────┘ ┴ └─┘ └──┘
st ──────────────────────────────────────────────────────────────────────┘└─
168 rw abv_sub abv, exact hi _ ik
id └─────┘ └─┘ └┘ └┘
src └─┘└─────┘┴ └────┘ └─┘ ┴
typ └─┘└─────┘┴└─┘ └────┘└┘└─┘└┘┴
doc └─┘ ┴ └────┘ └─┘ ┴
txt └─┘ ┴ └────┘ └─┘ ┴
par └─┘ ┴ └────┘ └─┘ ┴
pid ┴ ┴ ┴ └─┘ ┴
st ───────────────┘└──────────────┘
169 end
st └─┘
170
171 theorem cauchy₃ (hf : is_cau_seq abv f) {ε:α} (ε0 : ε > 0) :
id └────────┘ └─┘ ┴ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ └─┘ ┴ ┴ ┴ ┴
doc └────────┘
172 ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
173 let ⟨i, H⟩ := hf.cauchy₂ ε0 in ⟨i, λ j ij k jk, H _ _ (le_trans ij jk) ij⟩
id └─┘ ┴ ┴ └┘└──────┘ └┘ ┴ └┘ ┴ └┘ └──────┘ └┘ └┘ └┘
src └──────┘ └──────┘
typ └─┘ ┴ ┴ └┘└──────┘ └┘ ┴ └┘ ┴ └┘ └──────┘ └┘ └┘ └┘
174
175 end is_cau_seq
176
177 def cau_seq {α : Type*} [discrete_linear_ordered_field α]
id └───────────────────────────┘ ┴
src └───────────────────────────┘
typ └───────────────────────────┘ ┴
178 (β : Type*) [ring β] (abv : β → α) :=
id └──┘ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴
179 {f : ℕ → β // is_cau_seq abv f}
id ┴ ┴ ┴ ┴ └────────┘ └─┘ ┴
src ┴ ┴ └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ └─┘ ┴
doc └────────┘
180
181 namespace cau_seq
182 variables {α : Type*} [discrete_linear_ordered_field α]
id ┴ └───────────────────────────┘
src └───────────────────────────┘
typ ┴ └───────────────────────────┘
183
184 section ring
185 variables {β : Type*} [ring β] {abv : β → α}
id ┴└──┘
src └──┘
typ ┴└──┘
186
187 instance : has_coe_to_fun (cau_seq β abv) := ⟨_, subtype.val⟩
id └────────────┘ └─────┘ ┴ └─┘ └─────────┘
src └────────────┘ └─────┘ └─────────┘
typ └────────────┘ └─────┘ ┴ └─┘ └─────────┘
188
189 @[simp] theorem mk_to_fun (f) (hf : is_cau_seq abv f) :
id └────────┘ └─┘ ┴
src └────────┘
typ └────────┘ └─┘ ┴
doc └──┘ └────────┘
190 @coe_fn (cau_seq β abv) _ ⟨f, hf⟩ = f := rfl
id └────┘ └─────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └─┘
src └────┘ └─────┘ ┴ └─┘
typ └────┘ └─────┘ ┴ └─┘ ┴ └┘ ┴ ┴ └─┘
191
192 theorem ext {f g : cau_seq β abv} (h : ∀ i, f i = g i) : f = g :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
193 subtype.eq (funext h)
id └────────┘ └────┘ ┴
src └────────┘ └────┘
typ └────────┘ └────┘ ┴
194
195 theorem is_cau (f : cau_seq β abv) : is_cau_seq abv f := f.2
id └─────┘ ┴ └─┘ └────────┘ └─┘ ┴ ┴┴
src └─────┘ └────────┘ ┴
typ └─────┘ ┴ └─┘ └────────┘ └─┘ ┴ ┴┴
doc └────────┘
196
197 theorem cauchy (f : cau_seq β abv) :
id └─────┘ ┴ └─┘
src └─────┘
typ └─────┘ ┴ └─┘
198 ∀ {ε}, ε > 0 → ∃ i, ∀ j ≥ i, abv (f j - f i) < ε := f.2
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
199
200 def of_eq (f : cau_seq β abv) (g : ℕ → β) (e : ∀ i, f i = g i) : cau_seq β abv :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─┘
src └─────┘ ┴ ┴ └─────┘
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ └─┘
201 ⟨g, λ ε, by rw [show g = f, from (funext e).symm]; exact f.cauchy⟩
id ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └──────┘
src └──┘ ┴ ┴┴┴ └─────┘ └────┘┴ └─────┘ └────┘└──────┘
typ ┴ ┴ └──┘ ┴┴┴┴┴┴└─────┘ └────┘┴┴└─────┘ └────┘└──────┘
doc └──┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ └────┘
txt └──┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ └────┘
par └──┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ └────┘
pid └┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴
st └──────────────────────────────────┘└┘└──────────────┘
202
203 variable [is_absolute_value abv]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
204
205 theorem cauchy₂ (f : cau_seq β abv) {ε:α} : ε > 0 →
id └─────┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴
206 ∃ i, ∀ j k ≥ i, abv (f j - f k) < ε := f.2.cauchy₂
id ┴ ┴┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─────┘
src ┴ ┴ ┴ ┴ ┴ └─────┘
typ ┴ ┴┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─────┘
207
208 theorem cauchy₃ (f : cau_seq β abv) {ε:α} : ε > 0 →
id └─────┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴
209 ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε := f.2.cauchy₃
id ┴ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─────┘
src ┴ ┴ ┴ ┴ ┴ └─────┘
typ ┴ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─────┘
210
211 theorem bounded (f : cau_seq β abv) : ∃ r, ∀ i, abv (f i) < r :=
id └─────┘ ┴ └─┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴
212 begin
st └─────
213 cases f.cauchy zero_lt_one with i h,
id └──────┘ └─────────┘
src └────┘└──────┘┴└─────────┘└───────┘
typ └────┘└──────┘┴└─────────┘└───────┘
doc └────┘ ┴ └───────┘
txt └────┘ ┴ └───────┘
par └────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ────────────────────────────────────┘└─
214 let R := (finset.range (i+1)).sum (λ j, abv (f j)),
id └──────────┘ ┴┴ └─┘ ┴
src └───────┘ └──────────┘┴ ┴└──────┘ └──┘ ┴ ┴ └┘
typ └───────┘ └──────────┘┴ ┴┴└──────┘ └──┘└─┘┴ ┴┴ └┘
doc └───────┘ └──────────┘┴ └──────┘ └──┘ ┴ ┴ └┘
txt └───────┘ ┴ └──────┘ └──┘ ┴ ┴ └┘
par └───────┘ ┴ └──────┘ └──┘ ┴ ┴ └┘
pid └───┘┴└─┘ ┴ └──────┘ └──┘ ┴ ┴ └┘
st ───────────────────────────────────────────────────┘└─
215 have : ∀ j ≤ i, abv (f j) ≤ R,
id ┴ └─┘ ┴ ┴
src └─────┘ └───┘ ┴ ┴ ┴ └┘ ┴
typ └─────┘ └───┘┴ ┴└─┘┴ ┴┴ └┘ ┴┴
doc └─────┘ └───┘ ┴ ┴ ┴ └┘ ┴
txt └─────┘ └───┘ ┴ ┴ ┴ └┘ ┴
par └─────┘ └───┘ ┴ ┴ ┴ └┘ ┴
pid └───┘└┘ └───┘ ┴ ┴ ┴ └┘ ┴
st ──────────────────────────────┘└─
216 { intros j ij, change (λ j, abv (f j)) j ≤ R,
id └─┘ ┴ ┴ ┴
src └─────────┘ └─────┘ └──┘ ┴ ┴ └─┘ ┴ ┴
typ └─────────┘ └─────┘ └──┘└─┘┴ ┴┴ └─┘┴┴ ┴┴
doc └─────────┘ └─────┘ └──┘ ┴ ┴ └─┘ ┴ ┴
txt └─────────┘ └─────┘ └──┘ ┴ ┴ └─┘ ┴ ┴
par └─────────┘ └─────┘ └──┘ ┴ ┴ └─┘ ┴ ┴
pid └───┘ ┴ └──┘ ┴ ┴ └─┘ ┴ ┴
st ───┘└─────────┘└─────────────────────────────┘└─
217 apply finset.single_le_sum,
id └──────────────────┘
src └────┘└──────────────────┘
typ └────┘└──────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────┘└─
218 { intros, apply abv_nonneg abv },
id └────────┘ └─┘
src └────┘ └────┘└────────┘┴ ┴
typ └────┘ └────┘└────────┘┴└─┘┴
doc └────┘ └────┘ ┴ ┴
txt └────┘ └────┘ ┴ ┴
par └────┘ └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└────┘└─────────────────────┘└┘└
219 { rwa [finset.mem_range, nat.lt_succ_iff] } },
id └──────────────┘ └─────────────┘
src └───┘└──────────────┘└┘└─────────────┘└┘
typ └───┘└──────────────┘└┘└─────────────┘└┘
doc └───┘ └┘ └┘
txt └───┘ └┘ └┘
par └───┘ └┘ └┘
pid └┘ └┘ ┴┴
st ──────────────────────────┘└───────────────┘┴┴└──┘└
220 refine ⟨R + 1, λ j, _⟩,
id ┴
src └─────┘ ┴ └──┘ └────┘
typ └─────┘ ┴┴ └──┘ └────┘
doc └─────┘ ┴ └──┘ └────┘
txt └─────┘ ┴ └──┘ └────┘
par └─────┘ ┴ └──┘ └────┘
pid ┴ ┴ └──┘ └────┘
st ───────────────────────┘└─
221 cases lt_or_le j i with ij ij,
id └──────┘ ┴ ┴
src └────┘└──────┘┴ ┴ └─────────┘
typ └────┘└──────┘┴┴┴┴└─────────┘
doc └────┘ ┴ ┴ └─────────┘
txt └────┘ ┴ ┴ └─────────┘
par └────┘ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ └─────────┘
st ──────────────────────────────┘└─
222 { exact lt_of_le_of_lt (this _ (le_of_lt ij)) (lt_add_one _) },
id └────────────┘ └──┘ └──────┘ └┘ └────────┘
src └────┘└────────────┘┴ └─┘ └──────┘┴ └─┘ └────────┘└──┘
typ └────┘└────────────┘┴ └──┘└─┘ └──────┘┴└┘└─┘ └────────┘└──┘
doc └────┘ ┴ └─┘ ┴ └─┘ └──┘
txt └────┘ ┴ └─┘ ┴ └─┘ └──┘
par └────┘ ┴ └─┘ ┴ └─┘ └──┘
pid ┴ ┴ └─┘ ┴ └─┘ └─┘┴
st ───┘└─────────────────────────────────────────────────────────┘└┘└
223 { have := lt_of_le_of_lt (abv_add abv _ _)
id └────────────┘ └─────┘ └─┘
src └──────┘└────────────┘┴ └─────┘┴ └─────
typ └──────┘└────────────┘┴ └─────┘┴└─┘└─────
doc └──────┘ ┴ ┴ └─────
txt └──────┘ ┴ ┴ └─────
par └──────┘ ┴ ┴ └─────
pid └───┘└─┘ ┴ ┴ └─────
st ─────────────────────────────────────────────
224 (add_lt_add_of_le_of_lt (this _ (le_refl _)) (h _ ij)),
id └────────────────────┘ └──┘ └─────┘ ┴ └┘
src ─────┘ └────────────────────┘┴ └─┘ └─────┘└───┘ └─┘ └┘
typ ─────┘ └────────────────────┘┴ └──┘└─┘ └─────┘└───┘ ┴└─┘└┘└┘
doc ─────┘ ┴ └─┘ └───┘ └─┘ └┘
txt ─────┘ ┴ └─┘ └───┘ └─┘ └┘
par ─────┘ ┴ └─┘ └───┘ └─┘ └┘
pid ─────┘ ┴ └─┘ └───┘ └─┘ └┘
st ───────────────────────────────────────────────────────────┘└─
225 rw [add_sub, add_comm] at this, simpa }
id └─────┘ └──────┘
src └──┘└─────┘└┘└──────┘└───────┘ └────┘
typ └──┘└─────┘└┘└──────┘└───────┘ └────┘
doc └──┘ └┘ └───────┘ └────┘
txt └──┘ └┘ └───────┘ └────┘
par └──┘ └┘ └───────┘ └────┘
pid └┘ └┘ ┴└──────┘ ┴
st ──────────────┘└────────┘┴└──────┘└──────┘└─
226 end
st ──┘
227
228 theorem bounded' (f : cau_seq β abv) (x : α) : ∃ r > x, ∀ i, abv (f i) < r :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴
229 let ⟨r, h⟩ := f.bounded in
id └─┘ ┴ ┴ ┴└──────┘
src └──────┘
typ └─┘ ┴ ┴ ┴└──────┘
230 ⟨max r (x+1), lt_of_lt_of_le (lt_add_one _) (le_max_right _ _),
id └─┘ ┴┴ └────────────┘ └────────┘ └──────────┘
src └─┘ ┴ └────────────┘ └────────┘ └──────────┘
typ └─┘ ┴┴ └────────────┘ └────────┘ └──────────┘
231 λ i, lt_of_lt_of_le (h i) (le_max_left _ _)⟩
id ┴ └────────────┘ ┴ └─────────┘
src └────────────┘ └─────────┘
typ ┴ └────────────┘ ┴ └─────────┘
232
233 instance : has_add (cau_seq β abv) :=
id └─────┘ └─────┘ ┴ └─┘
src └─────┘ └─────┘
typ └─────┘ └─────┘ ┴ └─┘
234 ⟨λ f g, ⟨λ i, (f i + g i : β), λ ε ε0,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
235 let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma abv ε0,
id └─┘ └┘ └┘ └──────────────────────┘ └─┘ └┘
src └──────────────────────┘
typ └─┘ └┘ └┘ └──────────────────────┘ └─┘ └┘
236 ⟨i, H⟩ := exists_forall_ge_and (f.cauchy₃ δ0) (g.cauchy₃ δ0) in
id ┴ ┴ └──────────────────┘ ┴└──────┘ ┴└──────┘
src └──────────────────┘ └──────┘ └──────┘
typ ┴ ┴ └──────────────────┘ ┴└──────┘ ┴└──────┘
237 ⟨i, λ j ij, let ⟨H₁, H₂⟩ := H _ (le_refl _) in Hδ (H₁ _ ij) (H₂ _ ij)⟩⟩⟩
id ┴ └┘ └─┘ └┘ └┘ └─────┘ └┘ └┘
src └─────┘
typ ┴ └┘ └─┘ └┘ └┘ └─────┘ └┘ └┘
238
239 @[simp] theorem add_apply (f g : cau_seq β abv) (i : ℕ) : (f + g) i = f i + g i := rfl
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └─────┘ ┴ ┴ ┴ ┴ └─┘
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
240
241 variable (abv)
242
243 /-- The constant Cauchy sequence. -/
244 def const (x : β) : cau_seq β abv :=
id ┴ └─────┘ ┴ └─┘
src └─────┘
typ ┴ └─────┘ ┴ └─┘
245 ⟨λ i, x, λ ε ε0, ⟨0, λ j ij, by simpa [abv_zero abv] using ε0⟩⟩
id ┴ ┴ ┴ └┘ ┴ └┘ └──────┘ └─┘ └┘
src └─────┘└──────┘┴ └──────┘
typ ┴ ┴ ┴ └┘ ┴ └┘ └─────┘└──────┘┴└─┘└──────┘└┘
doc └─────┘ ┴ └──────┘
txt └─────┘ ┴ └──────┘
par └─────┘ ┴ └──────┘
pid ┴┴ ┴ ┴┴└────┘
st └────────────────────────────┘
246
247 variable {abv}
248
249 local notation `const` := const abv
id └───┘
src └───┘
typ └───┘
doc └───┘
250
251 @[simp] theorem const_apply (x : β) (i : ℕ) : (const x : ℕ → β) i = x := rfl
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ └───┘ ┴ ┴ └─┘
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘ └───┘
252
253 theorem const_inj {x y : β} : (const x : cau_seq β abv) = const y ↔ x = y :=
id ┴ └───┘ ┴ └─────┘ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └───┘ └─────┘ ┴ └───┘ ┴ ┴
typ ┴ └───┘ ┴ └─────┘ ┴ └─┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
254 ⟨λ h, congr_arg (λ f:cau_seq β abv, (f:ℕ→β) 0) h, congr_arg _⟩
id ┴ └───────┘ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───────┘
src └───────┘ └─────┘ ┴ └───────┘
typ ┴ └───────┘ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───────┘
255
256 instance : has_zero (cau_seq β abv) := ⟨const 0⟩
id └──────┘ └─────┘ ┴ └─┘ └───┘
src └──────┘ └─────┘ └───┘
typ └──────┘ └─────┘ ┴ └─┘ └───┘
doc └───┘
257 instance : has_one (cau_seq β abv) := ⟨const 1⟩
id └─────┘ └─────┘ ┴ └─┘ └───┘
src └─────┘ └─────┘ └───┘
typ └─────┘ └─────┘ ┴ └─┘ └───┘
doc └───┘
258 instance : inhabited (cau_seq β abv) := ⟨0⟩
id └───────┘ └─────┘ ┴ └─┘
src └───────┘ └─────┘
typ └───────┘ └─────┘ ┴ └─┘
259
260 @[simp] theorem zero_apply (i) : (0 : cau_seq β abv) i = 0 := rfl
id └─────┘ ┴ └─┘ ┴ ┴ └─┘
src └─────┘ ┴ └─┘
typ └─────┘ ┴ └─┘ ┴ ┴ └─┘
doc └──┘
261 @[simp] theorem one_apply (i) : (1 : cau_seq β abv) i = 1 := rfl
id └─────┘ ┴ └─┘ ┴ ┴ └─┘
src └─────┘ ┴ └─┘
typ └─────┘ ┴ └─┘ ┴ ┴ └─┘
doc └──┘
262
263 theorem const_add (x y : β) : const (x + y) = const x + const y :=
id ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴
src └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴
doc └───┘ └───┘ └───┘
264 ext $ λ i, rfl
id └─┘ ┴ └─┘
src └─┘ └─┘
typ └─┘ ┴ └─┘
265
266 instance : has_mul (cau_seq β abv) :=
id └─────┘ └─────┘ ┴ └─┘
src └─────┘ └─────┘
typ └─────┘ └─────┘ ┴ └─┘
267 ⟨λ f g, ⟨λ i, (f i * g i : β), λ ε ε0,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
268 let ⟨F, F0, hF⟩ := f.bounded' 0, ⟨G, G0, hG⟩ := g.bounded' 0,
id └─┘ └┘ ┴└───────┘ └┘ ┴└───────┘
src └───────┘ └───────┘
typ └─┘ └┘ ┴└───────┘ └┘ ┴└───────┘
269 ⟨δ, δ0, Hδ⟩ := rat_mul_continuous_lemma abv ε0,
id └┘ └┘ └──────────────────────┘ └─┘ └┘
src └──────────────────────┘
typ └┘ └┘ └──────────────────────┘ └─┘ └┘
270 ⟨i, H⟩ := exists_forall_ge_and (f.cauchy₃ δ0) (g.cauchy₃ δ0) in
id ┴ ┴ └──────────────────┘ ┴└──────┘ ┴└──────┘
src └──────────────────┘ └──────┘ └──────┘
typ ┴ ┴ └──────────────────┘ ┴└──────┘ ┴└──────┘
271 ⟨i, λ j ij, let ⟨H₁, H₂⟩ := H _ (le_refl _) in
id ┴ └┘ └─┘ └┘ └┘ └─────┘
src └─────┘
typ ┴ └┘ └─┘ └┘ └┘ └─────┘
272 Hδ (hF j) (hG i) (H₁ _ ij) (H₂ _ ij)⟩⟩⟩
id ┴ └┘ └┘
typ ┴ └┘ └┘
273
274 @[simp] theorem mul_apply (f g : cau_seq β abv) (i : ℕ) : (f * g) i = f i * g i := rfl
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └─────┘ ┴ ┴ ┴ ┴ └─┘
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
275
276 theorem const_mul (x y : β) : const (x * y) = const x * const y :=
id ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴
src └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴
doc └───┘ └───┘ └───┘
277 ext $ λ i, rfl
id └─┘ ┴ └─┘
src └─┘ └─┘
typ └─┘ ┴ └─┘
278
279 instance : has_neg (cau_seq β abv) :=
id └─────┘ └─────┘ ┴ └─┘
src └─────┘ └─────┘
typ └─────┘ └─────┘ ┴ └─┘
280 ⟨λ f, of_eq (const (-1) * f) (λ x, -f x) (λ i, by simp)⟩
id ┴ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴
src └───┘ └───┘ ┴ ┴ ┴ └──┘
typ ┴ └───┘ └───┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └──┘
doc └───┘ └──┘
txt └──┘
par └──┘
st └───┘
281
282 @[simp] theorem neg_apply (f : cau_seq β abv) (i) : (-f) i = -f i := rfl
id └─────┘ ┴ └─┘ ┴┴ ┴ ┴ ┴┴ ┴ └─┘
src └─────┘ ┴ ┴ ┴ └─┘
typ └─────┘ ┴ └─┘ ┴┴ ┴ ┴ ┴┴ ┴ └─┘
doc └──┘
283
284 theorem const_neg (x : β) : const (-x) = -const x :=
id ┴ └───┘ ┴┴ ┴ ┴└───┘ ┴
src └───┘ ┴ ┴ ┴└───┘
typ ┴ └───┘ ┴┴ ┴ ┴└───┘ ┴
doc └───┘ └───┘
285 ext $ λ i, rfl
id └─┘ ┴ └─┘
src └─┘ └─┘
typ └─┘ ┴ └─┘
286
287 instance : ring (cau_seq β abv) :=
id └──┘ └─────┘ ┴ └─┘
src └──┘ └─────┘
typ └──┘ └─────┘ ┴ └─┘
288 by refine {neg := has_neg.neg, add := (+), zero := 0, mul := (*), one := 1, ..};
id └─────────┘ ┴ ┴
src └─────┘ └─────┘└─────────┘└───────┘┴└────────────────────┘┴└───────────────┘
typ └─────┘ └─────┘└─────────┘└───────┘┴└────────────────────┘┴└───────────────┘
doc └─────┘ └─────┘ └───────┘ └────────────────────┘ └───────────────┘
txt └─────┘ └─────┘ └───────┘ └────────────────────┘ └───────────────┘
par └─────┘ └─────┘ └───────┘ └────────────────────┘ └───────────────┘
pid ┴ └─────┘ └───────┘ └────────────────────┘ └───────────────┘
st └──────────────────────────────────────────────────────────────────────────────
289 { intros, apply ext, simp [mul_add, mul_assoc, add_mul] }
id └─┘ └─────┘ └───────┘ └─────┘
src └────┘ └────┘└─┘ └────┘└─────┘└┘└───────┘└┘└─────┘└┘
typ └────┘ └────┘└─┘ └────┘└─────┘└┘└───────┘└┘└─────┘└┘
doc └────┘ └────┘ └────┘ └┘ └┘ └┘
txt └────┘ └────┘ └────┘ └┘ └┘ └┘
par └────┘ └────┘ └────┘ └┘ └┘ └┘
pid ┴ ┴┴ └┘ └┘ ┴┴
st ──┘└──────┘└─────────┘└───────────────────────────────────┘└┘
290
291 instance {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv] : comm_ring (cau_seq β abv) :=
id └───────┘ ┴ ┴ ┴ └───────────────┘ └─┘ └───────┘ └─────┘ ┴ └─┘
src └───────┘ └───────────────┘ └───────┘ └─────┘
typ └───────┘ ┴ ┴ ┴ └───────────────┘ └─┘ └───────┘ └─────┘ ┴ └─┘
doc └───────────────┘
292 { mul_comm := by intros; apply ext; simp [mul_left_comm, mul_comm],
id └─┘ └───────────┘ └──────┘
src └────┘ └────┘└─┘ └────┘└───────────┘└┘└──────┘┴
typ └────┘ └────┘└─┘ └────┘└───────────┘└┘└──────┘┴
doc └────┘ └────┘ └────┘ └┘ ┴
txt └────┘ └────┘ └────┘ └┘ ┴
par └────┘ └────┘ └────┘ └┘ ┴
pid ┴ ┴┴ └┘ ┴
st └────────────────────────────────────────────────┘
293 ..cau_seq.ring }
id └──────────┘
src └──────────┘
typ └──────────┘
294
295 theorem const_sub (x y : β) : const (x - y) = const x - const y :=
id ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴
src └───┘ ┴ ┴ └───┘ ┴ └───┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └───┘ ┴
doc └───┘ └───┘ └───┘
296 by rw [sub_eq_add_neg, const_add, const_neg, sub_eq_add_neg]
id └────────────┘ └───────┘ └───────┘ └────────────┘
src └──┘└────────────┘└┘└───────┘└┘└───────┘└┘└────────────┘└─
typ └──┘└────────────┘└┘└───────┘└┘└───────┘└┘└────────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ ┴└
st └─────────────────┘└─────────┘└─────────┘└──────────────┘┴└
297
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
298 @[simp] theorem sub_apply (f g : cau_seq β abv) (i : ℕ) : (f - g) i = f i - g i := rfl
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └─────┘ ┴ ┴ ┴ ┴ └─┘
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
299
300 /-- `lim_zero f` holds when `f` approaches 0. -/
301 def lim_zero (f : cau_seq β abv) := ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j) < ε
id └─────┘ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
302
303 theorem add_lim_zero {f g : cau_seq β abv}
id └─────┘ ┴ └─┘
src └─────┘
typ └─────┘ ┴ └─┘
304 (hf : lim_zero f) (hg : lim_zero g) : lim_zero (f + g)
id └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴
src └──────┘ └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘ └──────┘ └──────┘
305 | ε ε0 := (exists_forall_ge_and
id └┘ └──────────────────┘
src └──────────────────┘
typ └┘ └──────────────────┘
306 (hf _ $ half_pos ε0) (hg _ $ half_pos ε0)).imp $
id └┘ └──────┘ └┘ └──────┘ └─┘
src └──────┘ └──────┘ └─┘
typ └┘ └──────┘ └┘ └──────┘ └─┘
307 λ i H j ij, let ⟨H₁, H₂⟩ := H _ ij in
id ┴ ┴ ┴ └┘ └─┘ ┴ └┘
typ ┴ ┴ ┴ └┘ └─┘ ┴ └┘
308 by simpa [add_halves ε] using lt_of_le_of_lt (abv_add abv _ _) (add_lt_add H₁ H₂)
id └────────┘ ┴ └────────────┘ └─────┘ └─┘ └────────┘ └┘ └┘
src └─────┘└────────┘┴ └──────┘└────────────┘┴ └─────┘┴ └────┘ └────────┘┴ ┴ └─
typ └─────┘└────────┘┴┴└──────┘└────────────┘┴ └─────┘┴└─┘└────┘ └────────┘┴└┘┴└┘└─
doc └─────┘ ┴ └──────┘ ┴ ┴ └────┘ ┴ ┴ └─
txt └─────┘ ┴ └──────┘ ┴ ┴ └────┘ ┴ ┴ └─
par └─────┘ ┴ └──────┘ ┴ ┴ └────┘ ┴ ┴ └─
pid ┴┴ ┴ ┴┴└────┘ ┴ ┴ └────┘ ┴ ┴ ┴└
st └───────────────────────────────────────────────────────────────────────────────
309
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
310 theorem mul_lim_zero_right (f : cau_seq β abv) {g}
id └─────┘ ┴ └─┘
src └─────┘
typ └─────┘ ┴ └─┘
311 (hg : lim_zero g) : lim_zero (f * g)
id └──────┘ ┴ └──────┘ ┴ ┴ ┴
src └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘ └──────┘
312 | ε ε0 := let ⟨F, F0, hF⟩ := f.bounded' 0 in
id └┘ └─┘ └┘ ┴└───────┘
src └───────┘
typ └┘ └─┘ └┘ ┴└───────┘
313 (hg _ $ div_pos ε0 F0).imp $ λ i H j ij,
id └┘ └─────┘ └─┘ ┴ ┴ ┴ └┘
src └─────┘ └─┘
typ └┘ └─────┘ └─┘ ┴ ┴ ┴ └┘
314 by have := mul_lt_mul' (le_of_lt $ hF j) (H _ ij) (abv_nonneg abv _) F0;
id └─────────┘ └──────┘ └┘ ┴ ┴ └┘ └────────┘ └─┘ └┘
src └──────┘└─────────┘┴ └──────┘┴ ┴ ┴ └┘ └─┘ └┘ └────────┘┴ └──┘
typ └──────┘└─────────┘┴ └──────┘┴ ┴└┘┴┴└┘ ┴└─┘└┘└┘ └────────┘┴└─┘└──┘└┘
doc └──────┘ ┴ ┴ ┴ ┴ └┘ └─┘ └┘ ┴ └──┘
txt └──────┘ ┴ ┴ ┴ ┴ └┘ └─┘ └┘ ┴ └──┘
par └──────┘ ┴ ┴ ┴ ┴ └┘ └─┘ └┘ ┴ └──┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ └┘ └─┘ └┘ ┴ └──┘
st └──────────────────────────────────────────────────────────────────────
315 rwa [mul_comm F, div_mul_cancel _ (ne_of_gt F0), ← abv_mul abv] at this
id └──────┘ ┴ └────────────┘ └──────┘ └┘ └─────┘ └─┘
src └───┘└──────┘┴ └┘└────────────┘└─┘ └──────┘┴ └───┘└─────┘┴ └─────────
typ └───┘└──────┘┴┴└┘└────────────┘└─┘ └──────┘┴└┘└───┘└─────┘┴└─┘└─────────
doc └───┘ ┴ └┘ └─┘ ┴ └───┘ ┴ └─────────
txt └───┘ ┴ └┘ └─┘ ┴ └───┘ ┴ └─────────
par └───┘ ┴ └┘ └─┘ ┴ └───┘ ┴ └─────────
pid └┘ ┴ └┘ └─┘ ┴ └───┘ ┴ ┴└──────┘└
st ─────────┘└────────┘└──────────────────────────────┘└─────────────┘┴└────────
316
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
317 theorem mul_lim_zero_left {f} (g : cau_seq β abv)
id └─────┘ ┴ └─┘
src └─────┘
typ └─────┘ ┴ └─┘
318 (hg : lim_zero f) : lim_zero (f * g)
id └──────┘ ┴ └──────┘ ┴ ┴ ┴
src └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘ └──────┘
319 | ε ε0 := let ⟨G, G0, hG⟩ := g.bounded' 0 in
id └┘ └─┘ └┘ ┴└───────┘
src └───────┘
typ └┘ └─┘ └┘ ┴└───────┘
320 (hg _ $ div_pos ε0 G0).imp $ λ i H j ij,
id └┘ └─────┘ └─┘ ┴ ┴ ┴ └┘
src └─────┘ └─┘
typ └┘ └─────┘ └─┘ ┴ ┴ ┴ └┘
321 by have := mul_lt_mul'' (H _ ij) (hG j) (abv_nonneg abv _) (abv_nonneg abv _);
id └──────────┘ ┴ └┘ └┘ ┴ └────────┘ └─┘
src └──────┘└──────────┘┴ └─┘ └┘ ┴ └┘ ┴ └──┘ └────────┘┴ └─┘
typ └──────┘└──────────┘┴ ┴└─┘└┘└┘ └┘┴┴└┘ ┴ └──┘ └────────┘┴└─┘└─┘
doc └──────┘ ┴ └─┘ └┘ ┴ └┘ ┴ └──┘ ┴ └─┘
txt └──────┘ ┴ └─┘ └┘ ┴ └┘ ┴ └──┘ ┴ └─┘
par └──────┘ ┴ └─┘ └┘ ┴ └┘ ┴ └──┘ ┴ └─┘
pid └───┘└─┘ ┴ └─┘ └┘ ┴ └┘ ┴ └──┘ ┴ └─┘
st └────────────────────────────────────────────────────────────────────────────
322 rwa [div_mul_cancel _ (ne_of_gt G0), ← abv_mul abv] at this
id └────────────┘ └──────┘ └┘ └─────┘ └─┘
src └───┘└────────────┘└─┘ └──────┘┴ └───┘└─────┘┴ └─────────
typ └───┘└────────────┘└─┘ └──────┘┴└┘└───┘└─────┘┴└─┘└─────────
doc └───┘ └─┘ ┴ └───┘ ┴ └─────────
txt └───┘ └─┘ ┴ └───┘ ┴ └─────────
par └───┘ └─┘ ┴ └───┘ ┴ └─────────
pid └┘ └─┘ ┴ └───┘ ┴ ┴└──────┘└
st ─────────┘└────────────────────────────┘└─────────────┘┴└────────
323
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
324 theorem neg_lim_zero {f : cau_seq β abv} (hf : lim_zero f) : lim_zero (-f) :=
id └─────┘ ┴ └─┘ └──────┘ ┴ └──────┘ ┴┴
src └─────┘ └──────┘ └──────┘ ┴
typ └─────┘ ┴ └─┘ └──────┘ ┴ └──────┘ ┴┴
doc └──────┘ └──────┘
325 by rw ← neg_one_mul; exact mul_lim_zero_right _ hf
id └─────────┘ └────────────────┘ └┘
src └───┘└─────────┘ └────┘└────────────────┘└─┘ └
typ └───┘└─────────┘ └────┘└────────────────┘└─┘└┘└
doc └───┘└─────────┘ └────┘ └─┘ └
txt └───┘ └────┘ └─┘ └
par └───┘ └────┘ └─┘ └
pid └─┘ ┴ └─┘ └
st └────────────────────────────────────────────────
326
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
327 theorem sub_lim_zero {f g : cau_seq β abv}
id └─────┘ ┴ └─┘
src └─────┘
typ └─────┘ ┴ └─┘
328 (hf : lim_zero f) (hg : lim_zero g) : lim_zero (f - g) :=
id └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴
src └──────┘ └──────┘ └──────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘ └──────┘ └──────┘
329 add_lim_zero hf (neg_lim_zero hg)
id └──────────┘ └┘ └──────────┘ └┘
src └──────────┘ └──────────┘
typ └──────────┘ └┘ └──────────┘ └┘
330
331 theorem lim_zero_sub_rev {f g : cau_seq β abv} (hfg : lim_zero (f - g)) : lim_zero (g - f) :=
id └─────┘ ┴ └─┘ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
src └─────┘ └──────┘ ┴ └──────┘ ┴
typ └─────┘ ┴ └─┘ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘ └──────┘
332 by simpa using neg_lim_zero hfg
id └──────────┘ └─┘
src └──────────┘└──────────┘┴ └
typ └──────────┘└──────────┘┴└─┘└
doc └──────────┘ ┴ └
txt └──────────┘ ┴ └
par └──────────┘ ┴ └
pid ┴└────┘ ┴ └
st └─────────────────────────────
333
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
334 theorem zero_lim_zero : lim_zero (0 : cau_seq β abv)
id └──────┘ └─────┘ ┴ └─┘
src └──────┘ └─────┘
typ └──────┘ └─────┘ ┴ └─┘
doc └──────┘
335 | ε ε0 := ⟨0, λ j ij, by simpa [abv_zero abv] using ε0⟩
id ┴ └┘ └──────┘ └─┘ └┘
src └─────┘└──────┘┴ └──────┘
typ ┴ └┘ └─────┘└──────┘┴└─┘└──────┘└┘
doc └─────┘ ┴ └──────┘
txt └─────┘ ┴ └──────┘
par └─────┘ ┴ └──────┘
pid ┴┴ ┴ ┴┴└────┘
st └────────────────────────────┘
336
337 theorem const_lim_zero {x : β} : lim_zero (const x) ↔ x = 0 :=
id ┴ └──────┘ └───┘ ┴ ┴ ┴ ┴
src └──────┘ └───┘ ┴ ┴
typ ┴ └──────┘ └───┘ ┴ ┴ ┴ ┴
doc └──────┘ └───┘
338 ⟨λ H, (abv_eq_zero abv).1 $
id ┴ └─────────┘ └─┘ ┴
src └─────────┘ ┴
typ ┴ └─────────┘ └─┘ ┴
339 eq_of_le_of_forall_le_of_dense (abv_nonneg abv _) $
id └────────────────────────────┘ └────────┘ └─┘
src └────────────────────────────┘ └────────┘
typ └────────────────────────────┘ └────────┘ └─┘
340 λ ε ε0, let ⟨i, hi⟩ := H _ ε0 in le_of_lt $ hi _ (le_refl _),
id ┴ └┘ └─┘ └┘ ┴ └┘ └──────┘ └─────┘
src └──────┘ └─────┘
typ ┴ └┘ └─┘ └┘ ┴ └┘ └──────┘ └─────┘
341 λ e, e.symm ▸ zero_lim_zero⟩
id ┴ ┴└───┘ ┴ └───────────┘
src └───┘ ┴ └───────────┘
typ ┴ ┴└───┘ ┴ └───────────┘
342
343 instance equiv : setoid (cau_seq β abv) :=
id └────┘ └─────┘ ┴ └─┘
src └────┘ └─────┘
typ └────┘ └─────┘ ┴ └─┘
344 ⟨λ f g, lim_zero (f - g),
id ┴ ┴ └──────┘ ┴ ┴ ┴
src └──────┘ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
345 ⟨λ f, by simp [zero_lim_zero],
id ┴ └───────────┘
src └────┘└───────────┘┴
typ ┴ └────┘└───────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────────────────┘
346 λ f g h, by simpa using neg_lim_zero h,
id ┴ ┴ ┴ └──────────┘ ┴
src └──────────┘└──────────┘┴
typ ┴ ┴ ┴ └──────────┘└──────────┘┴┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st └─────────────────────────┘
347 λ f g h fg gh, by simpa using add_lim_zero fg gh⟩⟩
id ┴ ┴ ┴ └┘ └┘ └──────────┘ └┘ └┘
src └──────────┘└──────────┘┴ ┴
typ ┴ ┴ ┴ └┘ └┘ └──────────┘└──────────┘┴└┘┴└┘
doc └──────────┘ ┴ ┴
txt └──────────┘ ┴ ┴
par └──────────┘ ┴ ┴
pid ┴└────┘ ┴ ┴
st └─────────────────────────────┘
348
349 theorem equiv_def₃ {f g : cau_seq β abv} (h : f ≈ g) {ε:α} (ε0 : 0 < ε) :
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
350 ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - g j) < ε :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
351 (exists_forall_ge_and (h _ $ half_pos ε0) (f.cauchy₃ $ half_pos ε0)).imp $
id └──────────────────┘ ┴ └──────┘ └┘ ┴└──────┘ └──────┘ └┘ └─┘
src └──────────────────┘ └──────┘ └──────┘ └──────┘ └─┘
typ └──────────────────┘ ┴ └──────┘ └┘ ┴└──────┘ └──────┘ └┘ └─┘
352 λ i H j ij k jk, let ⟨h₁, h₂⟩ := H _ ij in
id ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴ └┘
typ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴ └┘
353 by have := lt_of_le_of_lt (abv_add abv (f j - g j) _) (add_lt_add h₁ (h₂ _ jk));
id └────────────┘ └─────┘ └─┘ ┴ ┴ ┴ ┴ └────────┘ └┘ └┘ └┘
src └──────┘└────────────┘┴ └─────┘┴ ┴ ┴ ┴┴┴ ┴ └───┘ └────────┘┴ ┴ └─┘ └┘
typ └──────┘└────────────┘┴ └─────┘┴└─┘┴ ┴┴ ┴┴┴┴┴┴└───┘ └────────┘┴└┘┴ └┘└─┘└┘└┘
doc └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘ └┘
txt └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘ └┘
par └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘ └┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └─┘ └┘
st └──────────────────────────────────────────────────────────────────────────────
354 rwa [sub_add_sub_cancel', add_halves] at this
id └─────────────────┘ └────────┘
src └───┘└─────────────────┘└┘└────────┘└─────────
typ └───┘└─────────────────┘└┘└────────┘└─────────
doc └───┘ └┘ └─────────
txt └───┘ └┘ └─────────
par └───┘ └┘ └─────────
pid └┘ └┘ ┴└──────┘└
st ───────┘└─────────────────┘└──────────┘┴└────────
355
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
356 theorem lim_zero_congr {f g : cau_seq β abv} (h : f ≈ g) : lim_zero f ↔ lim_zero g :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └─────┘ ┴ └──────┘ ┴ └──────┘
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘
357 ⟨λ l, by simpa using add_lim_zero (setoid.symm h) l,
id ┴ └──────────┘ └─────────┘ ┴ ┴
src └──────────┘└──────────┘┴ └─────────┘┴ └┘
typ ┴ └──────────┘└──────────┘┴ └─────────┘┴┴└┘┴
doc └──────────┘ ┴ ┴ └┘
txt └──────────┘ ┴ ┴ └┘
par └──────────┘ ┴ ┴ └┘
pid ┴└────┘ ┴ ┴ └┘
st └─────────────────────────────────────────┘
358 λ l, by simpa using add_lim_zero h l⟩
id ┴ └──────────┘ ┴ ┴
src └──────────┘└──────────┘┴ ┴
typ ┴ └──────────┘└──────────┘┴┴┴┴
doc └──────────┘ ┴ ┴
txt └──────────┘ ┴ ┴
par └──────────┘ ┴ ┴
pid ┴└────┘ ┴ ┴
st └───────────────────────────┘
359
360 theorem abv_pos_of_not_lim_zero {f : cau_seq β abv} (hf : ¬ lim_zero f) :
id └─────┘ ┴ └─┘ ┴ └──────┘ ┴
src └─────┘ ┴ └──────┘
typ └─────┘ ┴ └─┘ ┴ └──────┘ ┴
doc └──────┘
361 ∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ abv (f j) :=
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
362 begin
st └─────
363 haveI := classical.prop_decidable,
id └──────────────────────┘
src └───────┘└──────────────────────┘
typ └───────┘└──────────────────────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└─┘
st ──────────────────────────────────┘└─
364 by_contra nk,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └─┘
st ─────────────┘└─
365 refine hf (λ ε ε0, _),
id └┘
src └─────┘ ┴ └───────┘
typ └─────┘└┘┴ └───────┘
doc └─────┘ ┴ └───────┘
txt └─────┘ ┴ └───────┘
par └─────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ──────────────────────┘└─
366 simp [not_forall] at nk,
id └────────┘
src └────┘└────────┘└─────┘
typ └────┘└────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ────────────────────────┘└─
367 cases f.cauchy₃ (half_pos ε0) with i hi,
id └───────┘ └──────┘ └┘
src └────┘└───────┘┴ └──────┘┴ └─────────┘
typ └────┘└───────┘┴ └──────┘┴└┘└─────────┘
doc └────┘ ┴ ┴ └─────────┘
txt └────┘ ┴ ┴ └─────────┘
par └────┘ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ ┴└────────┘
st ────────────────────────────────────────┘└─
368 rcases nk _ (half_pos ε0) i with ⟨j, ij, hj⟩,
id └┘ └──────┘ └┘ ┴
src └─────┘ └─┘ └──────┘┴ └┘ └───────────────┘
typ └─────┘└┘└─┘ └──────┘┴└┘└┘┴└───────────────┘
doc └─────┘ └─┘ ┴ └┘ └───────────────┘
txt └─────┘ └─┘ ┴ └┘ └───────────────┘
par └─────┘ └─┘ ┴ └┘ └───────────────┘
pid ┴ └─┘ ┴ └┘ └───────────────┘
st ─────────────────────────────────────────────┘└─
369 refine ⟨j, λ k jk, _⟩,
id ┴
src └─────┘ └┘ └───────┘
typ └─────┘ ┴└┘ └───────┘
doc └─────┘ └┘ └───────┘
txt └─────┘ └┘ └───────┘
par └─────┘ └┘ └───────┘
pid ┴ └┘ └───────┘
st ──────────────────────┘└─
370 have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi j ij k jk) hj),
id └────────────┘ └─────┘ └─┘ └────────┘ └┘ ┴ └┘ ┴ └┘ └┘
src └──────┘└────────────┘┴ └─────┘┴ └────┘ └────────┘┴ ┴ ┴ ┴ ┴ └┘ ┴
typ └──────┘└────────────┘┴ └─────┘┴└─┘└────┘ └────────┘┴ └┘┴┴┴└┘┴┴┴└┘└┘└┘┴
doc └──────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
txt └──────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
par └──────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
pid └───┘└─┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────────────────────────┘└─
371 rwa [sub_add_cancel, add_halves] at this
id └────────────┘ └────────┘
src └───┘└────────────┘└┘└────────┘└────────┘
typ └───┘└────────────┘└┘└────────┘└────────┘
doc └───┘ └┘ └────────┘
txt └───┘ └┘ └────────┘
par └───┘ └┘ └────────┘
pid └┘ └┘ ┴└──────┘┴
st ────────────────────┘└──────────┘┴└───────┘
372 end
st └─┘
373
374 theorem of_near (f : ℕ → β) (g : cau_seq β abv)
id ┴ ┴ └─────┘ ┴ └─┘
src ┴ └─────┘
typ ┴ ┴ └─────┘ ┴ └─┘
375 (h : ∀ ε > 0, ∃ i, ∀ j ≥ i, abv (f j - g j) < ε) : is_cau_seq abv f
id ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └─┘ ┴
src ┴ ┴ ┴ ┴ └────────┘
typ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ └─┘ ┴
doc └────────┘
376 | ε ε0 :=
id └┘
typ └┘
377 let ⟨i, hi⟩ := exists_forall_ge_and
id └─┘ ┴ └──────────────────┘
src └──────────────────┘
typ └─┘ ┴ └──────────────────┘
378 (h _ (half_pos $ half_pos ε0)) (g.cauchy₃ $ half_pos ε0) in
id ┴ └──────┘ └──────┘ ┴└──────┘ └──────┘
src └──────┘ └──────┘ └──────┘ └──────┘
typ ┴ └──────┘ └──────┘ ┴└──────┘ └──────┘
379 ⟨i, λ j ij, begin
id ┴ └┘
typ ┴ └┘
st └─────
380 cases hi _ (le_refl _) with h₁ h₂, rw abv_sub abv at h₁,
id └┘ └─────┘ └─────┘ └─┘
src └────┘ └─┘ └─────┘└────────────┘ └─┘└─────┘┴ └────┘
typ └────┘└┘└─┘ └─────┘└────────────┘ └─┘└─────┘┴└─┘└────┘
doc └────┘ └─┘ └────────────┘ └─┘ ┴ └────┘
txt └────┘ └─┘ └────────────┘ └─┘ ┴ └────┘
par └────┘ └─┘ └────────────┘ └─┘ ┴ └────┘
pid ┴ └─┘ └─┘└─────────┘ ┴ ┴ └────┘
st ────────────────────────────────────┘└────────────────────┘└─
381 have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add (hi _ ij).1 h₁),
id └────────────┘ └─────┘ └─┘ └────────┘ └┘ └┘ └┘
src └──────┘└────────────┘┴ └─────┘┴ └────┘ └────────┘┴ └─┘ └──┘ ┴
typ └──────┘└────────────┘┴ └─────┘┴└─┘└────┘ └────────┘┴ └┘└─┘└┘└──┘└┘┴
doc └──────┘ ┴ ┴ └────┘ ┴ └─┘ └──┘ ┴
txt └──────┘ ┴ ┴ └────┘ ┴ └─┘ └──┘ ┴
par └──────┘ ┴ ┴ └────┘ ┴ └─┘ └──┘ ┴
pid └───┘└─┘ ┴ ┴ └────┘ ┴ └─┘ └──┘ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
382 have := lt_of_le_of_lt (abv_add abv _ _) (add_lt_add this (h₂ _ ij)),
id └────────────┘ └─────┘ └─┘ └────────┘ └──┘ └┘ └┘
src └──────┘└────────────┘┴ └─────┘┴ └────┘ └────────┘┴ ┴ └─┘ └┘
typ └──────┘└────────────┘┴ └─────┘┴└─┘└────┘ └────────┘┴└──┘┴ └┘└─┘└┘└┘
doc └──────┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └┘
txt └──────┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └┘
par └──────┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └┘
pid └───┘└─┘ ┴ ┴ └────┘ ┴ ┴ └─┘ └┘
st ───────────────────────────────────────────────────────────────────────┘└─
383 rwa [add_halves, add_halves, add_right_comm,
id └────────┘ └────────┘ └────────────┘
src └───┘└────────┘└┘└────────┘└┘└────────────┘└─
typ └───┘└────────┘└┘└────────┘└┘└────────────┘└─
doc └───┘ └┘ └┘ └─
txt └───┘ └┘ └┘ └─
par └───┘ └┘ └┘ └─
pid └┘ └┘ └┘ └─
st ──────────────────┘└──────────┘└──────────────┘└─
384 sub_add_sub_cancel, sub_add_sub_cancel] at this
id └────────────────┘ └────────────────┘
src ────────┘└────────────────┘└┘└────────────────┘└─────────
typ ────────┘└────────────────┘└┘└────────────────┘└─────────
doc ────────┘ └┘ └─────────
txt ────────┘ └┘ └─────────
par ────────┘ └┘ └─────────
pid ────────┘ └┘ ┴└──────┘└
st ──────────────────────────┘└──────────────────┘┴└────────
385 end⟩
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
386
387 lemma not_lim_zero_of_not_congr_zero {f : cau_seq _ abv} (hf : ¬ f ≈ 0) : ¬ lim_zero f :=
id └─────┘ └─┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └─────┘ ┴ ┴ ┴ └──────┘
typ └─────┘ └─┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘
388 assume : lim_zero f,
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
389 have lim_zero (f - 0), by simpa,
id └──────┘ ┴ ┴
src └──────┘ ┴ └───┘
typ └──────┘ ┴ ┴ └───┘
doc └──────┘ └───┘
txt └───┘
par └───┘
st └────┘
390 hf this
id └┘ └──┘
typ └┘ └──┘
391
392 lemma mul_equiv_zero (g : cau_seq _ abv) {f : cau_seq _ abv} (hf : f ≈ 0) : g * f ≈ 0 :=
id └─────┘ └─┘ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴ ┴
typ └─────┘ └─┘ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
393 have lim_zero (f - 0), from hf,
id └──────┘ ┴ ┴ └┘
src └──────┘ ┴
typ └──────┘ ┴ ┴ └┘
doc └──────┘
394 have lim_zero (g*f), from mul_lim_zero_right _ $ by simpa,
id └──────┘ ┴┴┴ └────────────────┘
src └──────┘ ┴ └────────────────┘ └───┘
typ └──────┘ ┴┴┴ └────────────────┘ └───┘
doc └──────┘ └───┘
txt └───┘
par └───┘
st └────┘
395 show lim_zero (g*f - 0), by simpa
id └──────┘ ┴┴┴ ┴
src └──────┘ ┴ ┴ └─────
typ └──────┘ ┴┴┴ ┴ └─────
doc └──────┘ └─────
txt └─────
par └─────
pid └
st └──────
396
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
397 lemma mul_not_equiv_zero {f g : cau_seq _ abv} (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) : ¬ (f * g) ≈ 0 :=
id └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
398 assume : lim_zero (f*g - 0),
id └──────┘ ┴┴┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴┴┴ ┴
doc └──────┘
399 have hlz : lim_zero (f*g), by simpa,
id └──────┘ ┴┴┴
src └──────┘ ┴ └───┘
typ └──────┘ ┴┴┴ └───┘
doc └──────┘ └───┘
txt └───┘
par └───┘
st └────┘
400 have hf' : ¬ lim_zero f, by simpa using (show ¬ lim_zero (f - 0), from hf),
id ┴ └──────┘ ┴ ┴ └──────┘ ┴ ┴ └┘
src ┴ └──────┘ └──────────┘ ┴ ┴└──────┘┴ ┴┴└────────┘ ┴
typ ┴ └──────┘ ┴ └──────────┘ ┴┴┴└──────┘┴ ┴┴┴└────────┘└┘┴
doc └──────┘ └──────────┘ ┴ ┴└──────┘┴ ┴ └────────┘ ┴
txt └──────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
par └──────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
pid ┴└────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
st └─────────────────────────────────────────────┘
401 have hg' : ¬ lim_zero g, by simpa using (show ¬ lim_zero (g - 0), from hg),
id ┴ └──────┘ ┴ ┴ └──────┘ ┴ └┘
src ┴ └──────┘ └──────────┘ ┴ ┴└──────┘┴ ┴ └────────┘ ┴
typ ┴ └──────┘ ┴ └──────────┘ ┴┴┴└──────┘┴ ┴┴ └────────┘└┘┴
doc └──────┘ └──────────┘ ┴ ┴└──────┘┴ ┴ └────────┘ ┴
txt └──────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
par └──────────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
pid ┴└────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
st └─────────────────────────────────────────────┘
402 begin
st └─────
403 rcases abv_pos_of_not_lim_zero hf' with ⟨a1, ha1, N1, hN1⟩,
id └─────────────────────┘ └─┘
src └─────┘└─────────────────────┘┴ └──────────────────────┘
typ └─────┘└─────────────────────┘┴└─┘└──────────────────────┘
doc └─────┘ ┴ └──────────────────────┘
txt └─────┘ ┴ └──────────────────────┘
par └─────┘ ┴ └──────────────────────┘
pid ┴ ┴ └──────────────────────┘
st ───────────────────────────────────────────────────────────┘└─
404 rcases abv_pos_of_not_lim_zero hg' with ⟨a2, ha2, N2, hN2⟩,
id └─────────────────────┘ └─┘
src └─────┘└─────────────────────┘┴ └──────────────────────┘
typ └─────┘└─────────────────────┘┴└─┘└──────────────────────┘
doc └─────┘ ┴ └──────────────────────┘
txt └─────┘ ┴ └──────────────────────┘
par └─────┘ ┴ └──────────────────────┘
pid ┴ ┴ └──────────────────────┘
st ───────────────────────────────────────────────────────────┘└─
405 have : a1 * a2 > 0, from mul_pos ha1 ha2,
id └┘ ┴ └┘ ┴ └─────┘ └─┘ └─┘
src └─────┘ ┴┴┴ ┴┴└┘ └───┘└─────┘┴ ┴
typ └─────┘└┘┴┴┴└┘┴┴└┘ └───┘└─────┘┴└─┘┴└─┘
doc └─────┘ ┴ ┴ ┴ └┘ └───┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └┘ └───┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ └┘ └───┘ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴┴ └───┘ ┴ ┴
st ───────────────────┘└────────────────────┘└─
406 cases hlz _ this with N hN,
id └─┘ └──┘
src └────┘ └─┘ └────────┘
typ └────┘└─┘└─┘└──┘└────────┘
doc └────┘ └─┘ └────────┘
txt └────┘ └─┘ └────────┘
par └────┘ └─┘ └────────┘
pid ┴ └─┘ └────────┘
st ───────────────────────────┘└─
407 let i := max N (max N1 N2),
id ┴ └─┘ └┘ └┘
src └───────┘ ┴ ┴ └─┘┴ ┴ ┴
typ └───────┘ ┴┴┴ └─┘┴└┘┴└┘┴
doc └───────┘ ┴ ┴ ┴ ┴ ┴
txt └───────┘ ┴ ┴ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴ ┴ ┴
pid └───┘┴└─┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────┘└─
408 have hN' := hN i (le_max_left _ _),
id └┘ ┴ └─────────┘
src └──────────┘ ┴ ┴ └─────────┘└───┘
typ └──────────┘└┘┴┴┴ └─────────┘└───┘
doc └──────────┘ ┴ ┴ └───┘
txt └──────────┘ ┴ ┴ └───┘
par └──────────┘ ┴ ┴ └───┘
pid └──────┘┴└─┘ ┴ ┴ └───┘
st ───────────────────────────────────┘└─
409 have hN1' := hN1 i (le_trans (le_max_left _ _) (le_max_right _ _)),
id └─┘ ┴ └──────┘ └─────────┘ └──────────┘
src └───────────┘ ┴ ┴ └──────┘┴ └─────────┘└────┘ └──────────┘└────┘
typ └───────────┘└─┘┴┴┴ └──────┘┴ └─────────┘└────┘ └──────────┘└────┘
doc └───────────┘ ┴ ┴ ┴ └────┘ └────┘
txt └───────────┘ ┴ ┴ ┴ └────┘ └────┘
par └───────────┘ ┴ ┴ ┴ └────┘ └────┘
pid └───────┘┴└─┘ ┴ ┴ ┴ └────┘ └────┘
st ───────────────────────────────────────────────────────────────────┘└─
410 have hN1' := hN2 i (le_trans (le_max_right _ _) (le_max_right _ _)),
id └─┘ ┴ └──────┘ └──────────┘
src └───────────┘ ┴ ┴ └──────┘┴ └────┘ └──────────┘└────┘
typ └───────────┘└─┘┴┴┴ └──────┘┴ └────┘ └──────────┘└────┘
doc └───────────┘ ┴ ┴ ┴ └────┘ └────┘
txt └───────────┘ ┴ ┴ ┴ └────┘ └────┘
par └───────────┘ ┴ ┴ ┴ └────┘ └────┘
pid └───────┘┴└─┘ ┴ ┴ ┴ └────┘ └────┘
st ────────────────────────────────────────────────────────────────────┘└─
411 apply not_le_of_lt hN',
id └──────────┘ └─┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴└─┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────┘└─
412 change _ ≤ abv (_ * _),
id ┴ └─┘
src └───────┘┴┴ ┴ └┘ └─┘
typ └───────┘┴┴└─┘┴ └┘ └─┘
doc └───────┘ ┴ ┴ └┘ └─┘
txt └───────┘ ┴ ┴ └┘ └─┘
par └───────┘ ┴ ┴ └┘ └─┘
pid └─┘ ┴ ┴ └┘ └─┘
st ───────────────────────┘└─
413 rw is_absolute_value.abv_mul abv,
id └───────────────────────┘ └─┘
src └─┘└───────────────────────┘┴
typ └─┘└───────────────────────┘┴└─┘
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ─────────────────────────────────┘└─
414 apply mul_le_mul; try { assumption },
id └────────┘
src └────┘└────────┘ └────┘└─────────┘┴
typ └────┘└────────┘ └────┘└─────────┘┴
doc └────┘ └────┘└─────────┘┴
txt └────┘ └────┘└─────────┘┴
par └────┘ └────┘└─────────┘┴
pid ┴ └─────────────┘
st ────────────────────────┘└──────────┘└┘└
415 { apply le_of_lt ha2 },
id └──────┘ └─┘
src └────┘└──────┘┴ ┴
typ └────┘└──────┘┴└─┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└─────────────────┘└┘└
416 { apply is_absolute_value.abv_nonneg abv }
id └──────────────────────────┘ └─┘
src └────┘└──────────────────────────┘┴ ┴
typ └────┘└──────────────────────────┘┴└─┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────────────────┘└─
417 end
st ──┘
418
419 theorem const_equiv {x y : β} : const x ≈ const y ↔ x = y :=
id ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
420 show lim_zero _ ↔ _, by rw [← const_sub, const_lim_zero, sub_eq_zero]
id └──────┘ ┴ └───────┘ └────────────┘ └─────────┘
src └──────┘ ┴ └────┘└───────┘└┘└────────────┘└┘└─────────┘└─
typ └──────┘ ┴ └────┘└───────┘└┘└────────────┘└┘└─────────┘└─
doc └──────┘ └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid └──┘ └┘ └┘ ┴└
st └──────────────┘└──────────────┘└───────────┘┴└
421
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
422 end ring
423
424 section comm_ring
425 variables {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv]
id └───────┘ └───────────────┘
src └───────┘ └───────────────┘
typ └───────┘ └───────────────┘
doc └───────────────┘
426
427 lemma mul_equiv_zero' (g : cau_seq _ abv) {f : cau_seq _ abv} (hf : f ≈ 0) : f * g ≈ 0 :=
id └─────┘ └─┘ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴ ┴
typ └─────┘ └─┘ └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
428 by rw mul_comm; apply mul_equiv_zero _ hf
id └──────┘ └────────────┘ └┘
src └─┘└──────┘ └────┘└────────────┘└─┘ └
typ └─┘└──────┘ └────┘└────────────┘└─┘└┘└
doc └─┘ └────┘ └─┘ └
txt └─┘ └────┘ └─┘ └
par └─┘ └────┘ └─┘ └
pid ┴ ┴ └─┘ └
st └───────────────────────────────────────
429
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
430 end comm_ring
431
432 section integral_domain
433 variables {β : Type*} [integral_domain β] (abv : β → α) [is_absolute_value abv]
id └─────────────┘ └───────────────┘
src └─────────────┘ └───────────────┘
typ └─────────────┘ └───────────────┘
doc └───────────────┘
434
435 lemma one_not_equiv_zero : ¬ (const abv 1) ≈ (const abv 0) :=
id ┴ └───┘ └─┘ ┴ └───┘ └─┘
src ┴ └───┘ ┴ └───┘
typ ┴ └───┘ └─┘ ┴ └───┘ └─┘
doc └───┘ └───┘
436 assume h,
id ┴
typ ┴
437 have ∀ ε > 0, ∃ i, ∀ k, k ≥ i → abv (1 - 0) < ε, from h,
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
438 have h1 : abv 1 ≤ 0, from le_of_not_gt $
id └─┘ ┴ └──────────┘
src ┴ └──────────┘
typ └─┘ ┴ └──────────┘
439 assume h2 : abv 1 > 0,
id └─┘ ┴
src ┴
typ └─┘ ┴
440 exists.elim (this _ h2) $ λ i hi,
id └─────────┘ └──┘ └┘ ┴ └┘
src └─────────┘
typ └─────────┘ └──┘ └┘ ┴ └┘
441 lt_irrefl (abv 1) $ by simpa using hi _ (le_refl _),
id └───────┘ └─┘ └┘ └─────┘
src └───────┘ └──────────┘ └─┘ └─────┘└─┘
typ └───────┘ └─┘ └──────────┘└┘└─┘ └─────┘└─┘
doc └──────────┘ └─┘ └─┘
txt └──────────┘ └─┘ └─┘
par └──────────┘ └─┘ └─┘
pid ┴└────┘ └─┘ └─┘
st └───────────────────────────┘
442 have h2 : abv 1 ≥ 0, from is_absolute_value.abv_nonneg _ _,
id └─┘ ┴ └──────────────────────────┘
src ┴ └──────────────────────────┘
typ └─┘ ┴ └──────────────────────────┘
443 have abv 1 = 0, from le_antisymm h1 h2,
id └─┘ ┴ └─────────┘ └┘ └┘
src ┴ └─────────┘
typ └─┘ ┴ └─────────┘ └┘ └┘
444 have (1 : β) = 0, from (is_absolute_value.abv_eq_zero abv).1 this,
id ┴ ┴ └───────────────────────────┘ └─┘ ┴ └──┘
src ┴ └───────────────────────────┘ ┴
typ ┴ ┴ └───────────────────────────┘ └─┘ ┴ └──┘
445 absurd this one_ne_zero
id └────┘ └──┘ └─────────┘
src └────┘ └─────────┘
typ └────┘ └──┘ └─────────┘
446
447 end integral_domain
448
449 section discrete_field
450 variables {β : Type*} [discrete_field β] {abv : β → α} [is_absolute_value abv]
id └────────────┘ └───────────────┘
src └────────────┘ └───────────────┘
typ └────────────┘ └───────────────┘
doc └───────────────┘
451
452 theorem inv_aux {f : cau_seq β abv} (hf : ¬ lim_zero f) :
id └─────┘ ┴ └─┘ ┴ └──────┘ ┴
src └─────┘ ┴ └──────┘
typ └─────┘ ┴ └─┘ ┴ └──────┘ ┴
doc └──────┘
453 ∀ ε > 0, ∃ i, ∀ j ≥ i, abv ((f j)⁻¹ - (f i)⁻¹) < ε | ε ε0 :=
id ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘
src ┴ ┴ └┘ ┴ └┘ ┴
typ ┴ ┴ ┴┴ ┴ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘
454 let ⟨K, K0, HK⟩ := abv_pos_of_not_lim_zero hf,
id └─┘ └┘ └┘ └─────────────────────┘ └┘
src └─────────────────────┘
typ └─┘ └┘ └┘ └─────────────────────┘ └┘
455 ⟨δ, δ0, Hδ⟩ := rat_inv_continuous_lemma abv ε0 K0,
id └┘ └┘ └──────────────────────┘ └─┘
src └──────────────────────┘
typ └┘ └┘ └──────────────────────┘ └─┘
456 ⟨i, H⟩ := exists_forall_ge_and HK (f.cauchy₃ δ0) in
id ┴ ┴ └──────────────────┘ ┴└──────┘
src └──────────────────┘ └──────┘
typ ┴ ┴ └──────────────────┘ ┴└──────┘
457 ⟨i, λ j ij, let ⟨iK, H'⟩ := H _ (le_refl _) in Hδ (H _ ij).1 iK (H' _ ij)⟩
id ┴ └┘ └─┘ └┘ └┘ └─────┘ └┘ ┴ └┘
src └─────┘ ┴
typ ┴ └┘ └─┘ └┘ └┘ └─────┘ └┘ ┴ └┘
458
459 def inv (f) (hf : ¬ lim_zero f) : cau_seq β abv := ⟨_, inv_aux hf⟩
id ┴ └──────┘ ┴ └─────┘ ┴ └─┘ └─────┘ └┘
src ┴ └──────┘ └─────┘ └─────┘
typ ┴ └──────┘ ┴ └─────┘ ┴ └─┘ └─────┘ └┘
doc └──────┘
460
461 @[simp] theorem inv_apply {f : cau_seq β abv} (hf i) : inv f hf i = (f i)⁻¹ := rfl
id └─────┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └─┘
src └─────┘ └─┘ ┴ └┘ └─┘
typ └─────┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └─┘
doc └──┘
462
463 theorem inv_mul_cancel {f : cau_seq β abv} (hf) : inv f hf * f ≈ 1 :=
id └─────┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴
src └─────┘ └─┘ ┴ ┴
typ └─────┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴
464 λ ε ε0, let ⟨K, K0, i, H⟩ := abv_pos_of_not_lim_zero hf in
id ┴ └┘ └─┘ ┴ └─────────────────────┘ └┘
src └─────────────────────┘
typ ┴ └┘ └─┘ ┴ └─────────────────────┘ └┘
465 ⟨i, λ j ij,
id ┴ └┘
typ ┴ └┘
466 by simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)),
id └─────┘ └─┘ └────────────┘ └┘ ┴ └┘
src └─────┘ └─────┘┴ └──┘ └────────────┘┴ ┴ └─┘ └───
typ └─────┘ └─────┘┴└─┘└──┘ └────────────┘┴└┘┴ ┴└─┘└┘└───
doc └─────┘ ┴ └──┘ ┴ ┴ └─┘ └───
txt └─────┘ ┴ └──┘ ┴ ┴ └─┘ └───
par └─────┘ ┴ └──┘ ┴ ┴ └─┘ └───
pid ┴┴ ┴ └──┘ ┴ ┴ └─┘ └───
st └─────────────────────────────────────────────────────
467 abv_zero abv] using ε0⟩
id └──────┘ └─┘ └┘
src ───┘└──────┘┴ └──────┘
typ ───┘└──────┘┴└─┘└──────┘└┘
doc ───┘ ┴ └──────┘
txt ───┘ ┴ └──────┘
par ───┘ ┴ └──────┘
pid ───┘ ┴ ┴┴└────┘
st ─────────────────────────┘
468
469 theorem const_inv {x : β} (hx : x ≠ 0) : const abv (x⁻¹) = inv (const abv x) (by rwa const_lim_zero) :=
id ┴ ┴ ┴ └───┘ └─┘ ┴└┘ ┴ └─┘ └───┘ └─┘ ┴ └────────────┘
src ┴ └───┘ └┘ ┴ └─┘ └───┘ └──┘└────────────┘
typ ┴ ┴ ┴ └───┘ └─┘ ┴└┘ ┴ └─┘ └───┘ └─┘ ┴ └──┘└────────────┘
doc └───┘ └───┘ └──┘
txt └──┘
par └──┘
pid ┴
st └─────────────────┘
470 ext (assume n, by simp[inv_apply, const_apply])
id └─┘ ┴ └───────┘ └─────────┘
src └─┘ └───┘└───────┘└┘└─────────┘┴
typ └─┘ ┴ └───┘└───────┘└┘└─────────┘┴
doc └───┘ └┘ ┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid ┴ └┘ ┴
st └───────────────────────────┘
471
472 end discrete_field
473
474 section abs
475 local notation `const` := const abs
id └───┘ └─┘
src └───┘ └─┘
typ └───┘ └─┘
doc └───┘
476
477 /-- The entries of a positive Cauchy sequence eventually have a positive lower bound. -/
478 def pos (f : cau_seq α abs) : Prop := ∃ K > 0, ∃ i, ∀ j ≥ i, K ≤ f j
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
479
480 theorem not_lim_zero_of_pos {f : cau_seq α abs} : pos f → ¬ lim_zero f
id └─────┘ ┴ └─┘ └─┘ ┴ ┴ ┴ └──────┘ ┴
src └─────┘ └─┘ └─┘ ┴ └──────┘
typ └─────┘ ┴ └─┘ └─┘ ┴ ┴ ┴ └──────┘ ┴
doc └─┘ └──────┘
481 | ⟨F, F0, hF⟩ H :=
id └┘ └┘ ┴
typ └┘ └┘ ┴
482 let ⟨i, h⟩ := exists_forall_ge_and hF (H _ F0),
id └─┘ ┴ └──────────────────┘
src └──────────────────┘
typ └─┘ ┴ └──────────────────┘
483 ⟨h₁, h₂⟩ := h _ (le_refl _) in
id └┘ └┘ └─────┘
src └─────┘
typ └┘ └┘ └─────┘
484 not_lt_of_le h₁ (abs_lt.1 h₂).2
id └──────────┘ └────┘┴ ┴
src └──────────┘ └────┘┴ ┴
typ └──────────┘ └────┘┴ ┴
485
486 theorem const_pos {x : α} : pos (const x) ↔ 0 < x :=
id ┴ └─┘ └───┘ ┴ ┴ ┴ ┴
src └─┘ └───┘ ┴ ┴
typ ┴ └─┘ └───┘ ┴ ┴ ┴ ┴
doc └─┘ └───┘
487 ⟨λ ⟨K, K0, i, h⟩, lt_of_lt_of_le K0 (h _ (le_refl _)),
id ┴ └┘ ┴ └────────────┘ └─────┘
src └────────────┘ └─────┘
typ ┴ └┘ ┴ └────────────┘ └─────┘
488 λ h, ⟨x, h, 0, λ j _, le_refl _⟩⟩
id ┴ ┴ ┴ ┴ ┴ └─────┘
src └─────┘
typ ┴ ┴ ┴ ┴ ┴ └─────┘
489
490 theorem add_pos {f g : cau_seq α abs} : pos f → pos g → pos (f + g)
id └─────┘ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘ └─┘ └─┘ ┴ └─┘ └─┘ ┴
typ └─────┘ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─┘ └─┘
491 | ⟨F, F0, hF⟩ ⟨G, G0, hG⟩ :=
id └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘
492 let ⟨i, h⟩ := exists_forall_ge_and hF hG in
id └─┘ ┴ ┴ └──────────────────┘
src └──────────────────┘
typ └─┘ ┴ ┴ └──────────────────┘
493 ⟨_, _root_.add_pos F0 G0, i,
id └────────────┘
src └────────────┘
typ └────────────┘
494 λ j ij, let ⟨h₁, h₂⟩ := h _ ij in add_le_add h₁ h₂⟩
id ┴ └┘ └─┘ └┘ └┘ └┘ └────────┘
src └────────┘
typ ┴ └┘ └─┘ └┘ └┘ └┘ └────────┘
495
496 theorem pos_add_lim_zero {f g : cau_seq α abs} : pos f → lim_zero g → pos (f + g)
id └─────┘ ┴ └─┘ └─┘ ┴ ┴ └──────┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘ └─┘ └─┘ └──────┘ └─┘ ┴
typ └─────┘ ┴ └─┘ └─┘ ┴ ┴ └──────┘ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └──────┘ └─┘
497 | ⟨F, F0, hF⟩ H :=
id └┘ └┘ ┴
typ └┘ └┘ ┴
498 let ⟨i, h⟩ := exists_forall_ge_and hF (H _ (half_pos F0)) in
id └─┘ ┴ └──────────────────┘ └──────┘
src └──────────────────┘ └──────┘
typ └─┘ ┴ └──────────────────┘ └──────┘
499 ⟨_, half_pos F0, i, λ j ij, begin
id └──────┘ ┴ └┘
src └──────┘
typ └──────┘ ┴ └┘
st └─────
500 cases h j ij with h₁ h₂,
id ┴ ┴ └┘
src └────┘ ┴ ┴ └─────────┘
typ └────┘┴┴┴┴└┘└─────────┘
doc └────┘ ┴ ┴ └─────────┘
txt └────┘ ┴ ┴ └─────────┘
par └────┘ ┴ ┴ └─────────┘
pid ┴ ┴ ┴ └─────────┘
st ──────────────────────────┘└─
501 have := add_le_add h₁ (le_of_lt (abs_lt.1 h₂).1),
id └────────┘ └┘ └──────┘ └────┘ └┘
src └──────┘└────────┘┴ ┴ └──────┘┴ └────┘└─┘ └──┘
typ └──────┘└────────┘┴└┘┴ └──────┘┴ └────┘└─┘└┘└──┘
doc └──────┘ ┴ ┴ ┴ └─┘ └──┘
txt └──────┘ ┴ ┴ ┴ └─┘ └──┘
par └──────┘ ┴ ┴ ┴ └─┘ └──┘
pid └───┘└─┘ ┴ ┴ ┴ └─┘ └──┘
st ───────────────────────────────────────────────────┘└─
502 rwa [← sub_eq_add_neg, sub_self_div_two] at this
id └────────────┘ └──────────────┘
src └─────┘└────────────┘└┘└──────────────┘└─────────
typ └─────┘└────────────┘└┘└──────────────┘└─────────
doc └─────┘ └┘ └─────────
txt └─────┘ └┘ └─────────
par └─────┘ └┘ └─────────
pid └──┘ └┘ ┴└──────┘└
st ────────────────────────┘└────────────────┘┴└────────
503 end⟩
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
504
505 theorem mul_pos {f g : cau_seq α abs} : pos f → pos g → pos (f * g)
id └─────┘ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘ └─┘ └─┘ ┴ └─┘ └─┘ ┴
typ └─────┘ ┴ └─┘ └─┘ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴
doc └─┘ └─┘ └─┘
506 | ⟨F, F0, hF⟩ ⟨G, G0, hG⟩ :=
id └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘
507 let ⟨i, h⟩ := exists_forall_ge_and hF hG in
id └─┘ ┴ ┴ └──────────────────┘
src └──────────────────┘
typ └─┘ ┴ ┴ └──────────────────┘
508 ⟨_, _root_.mul_pos F0 G0, i,
id └────────────┘
src └────────────┘
typ └────────────┘
509 λ j ij, let ⟨h₁, h₂⟩ := h _ ij in
id ┴ └┘ └─┘ └┘ └┘ └┘
typ ┴ └┘ └─┘ └┘ └┘ └┘
510 mul_le_mul h₁ h₂ (le_of_lt G0) (le_trans (le_of_lt F0) h₁)⟩
id └────────┘ └──────┘ └──────┘ └──────┘
src └────────┘ └──────┘ └──────┘ └──────┘
typ └────────┘ └──────┘ └──────┘ └──────┘
511
512 theorem trichotomy (f : cau_seq α abs) : pos f ∨ lim_zero f ∨ pos (-f) :=
id └─────┘ ┴ └─┘ └─┘ ┴ ┴ └──────┘ ┴ ┴ └─┘ ┴┴
src └─────┘ └─┘ └─┘ ┴ └──────┘ ┴ └─┘ ┴
typ └─────┘ ┴ └─┘ └─┘ ┴ ┴ └──────┘ ┴ ┴ └─┘ ┴┴
doc └─┘ └──────┘ └─┘
513 begin
st └─────
514 cases classical.em (lim_zero f); simp *,
id └──────────┘ └──────┘ ┴
src └────┘└──────────┘┴ └──────┘┴ ┴ └────┘
typ └────┘└──────────┘┴ └──────┘┴┴┴ └────┘
doc └────┘ ┴ └──────┘┴ ┴ └────┘
txt └────┘ ┴ ┴ ┴ └────┘
par └────┘ ┴ ┴ ┴ └────┘
pid ┴ ┴ ┴ ┴ ┴┴
st ────────────────────────────────────────┘└─
515 rcases abv_pos_of_not_lim_zero h with ⟨K, K0, hK⟩,
id └─────────────────────┘ ┴
src └─────┘└─────────────────────┘┴ └───────────────┘
typ └─────┘└─────────────────────┘┴┴└───────────────┘
doc └─────┘ ┴ └───────────────┘
txt └─────┘ ┴ └───────────────┘
par └─────┘ ┴ └───────────────┘
pid ┴ ┴ └───────────────┘
st ──────────────────────────────────────────────────┘└─
516 rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩,
id └──────────────────┘ └┘ └───────┘ └┘
src └─────┘└──────────────────┘┴ ┴ └───────┘┴ └────────────┘
typ └─────┘└──────────────────┘┴└┘┴ └───────┘┴└┘└────────────┘
doc └─────┘ ┴ ┴ ┴ └────────────┘
txt └─────┘ ┴ ┴ ┴ └────────────┘
par └─────┘ ┴ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ ┴ └────────────┘
st ───────────────────────────────────────────────────────────┘└─
517 refine (le_total 0 (f i)).imp _ _;
id └──────┘ ┴ ┴
src └─────┘ └──────┘└─┘ ┴ └────────┘
typ └─────┘ └──────┘└─┘ ┴┴┴└────────┘
doc └─────┘ └─┘ ┴ └────────┘
txt └─────┘ └─┘ ┴ └────────┘
par └─────┘ └─┘ ┴ └────────┘
pid ┴ └─┘ ┴ └────────┘
st ─────────────────────────────────────
518 refine (λ h, ⟨K, K0, i, λ j ij, _⟩);
id ┴ └┘ ┴
src └─────┘ └──┘ └┘ └┘ └┘ └────────┘
typ └─────┘ └──┘ ┴└┘└┘└┘┴└┘ └────────┘
doc └─────┘ └──┘ └┘ └┘ └┘ └────────┘
txt └─────┘ └──┘ └┘ └┘ └┘ └────────┘
par └─────┘ └──┘ └┘ └┘ └┘ └────────┘
pid ┴ └──┘ └┘ └┘ └┘ └────────┘
st ─────────────────────────────────────────
519 have := (hi _ ij).1;
id └┘ └┘
src └──────┘ └─┘ └─┘
typ └──────┘ └┘└─┘└┘└─┘
doc └──────┘ └─┘ └─┘
txt └──────┘ └─┘ └─┘
par └──────┘ └─┘ └─┘
pid └───┘└─┘ └─┘ ┴└┘
st ─────────────────────────
520 cases hi _ (le_refl _) with h₁ h₂,
id └┘ └─────┘
src └────┘ └─┘ └─────┘└────────────┘
typ └────┘└┘└─┘ └─────┘└────────────┘
doc └────┘ └─┘ └────────────┘
txt └────┘ └─┘ └────────────┘
par └────┘ └─┘ └────────────┘
pid ┴ └─┘ └─┘└─────────┘
st ────────────────────────────────────┘└─
521 { rwa abs_of_nonneg at this,
id └───────────┘
src └──┘└───────────┘└──────┘
typ └──┘└───────────┘└──────┘
doc └──┘ └──────┘
txt └──┘ └──────┘
par └──┘ └──────┘
pid ┴ └──────┘
st ───┘└───────────────────────┘└─
522 rw abs_of_nonneg h at h₁,
id └───────────┘ ┴
src └─┘└───────────┘┴ └────┘
typ └─┘└───────────┘┴┴└────┘
doc └─┘ ┴ └────┘
txt └─┘ ┴ └────┘
par └─┘ ┴ └────┘
pid ┴ ┴ └────┘
st ───────────────────────────┘└─
523 exact (le_add_iff_nonneg_right _).1
id └─────────────────────┘
src └────┘ └─────────────────────┘└─────
typ └────┘ └─────────────────────┘└─────
doc └────┘ └─────
txt └────┘ └─────
par └────┘ └─────
pid ┴ └─────
st ────────────────────────────────────────
524 (le_trans h₁ $ neg_le_sub_iff_le_add'.1 $
id └──────┘ └┘ └────────────────────┘
src ─────┘ └──────┘┴ ┴ ┴└────────────────────┘└─┘ └
typ ─────┘ └──────┘┴└┘┴ ┴└────────────────────┘└─┘ └
doc ─────┘ ┴ ┴ ┴ └─┘ └
txt ─────┘ ┴ ┴ ┴ └─┘ └
par ─────┘ ┴ ┴ ┴ └─┘ └
pid ─────┘ ┴ ┴ ┴ └─┘ └
st ────────────────────────────────────────────────
525 le_of_lt (abs_lt.1 $ h₂ _ ij).1) },
id └──────┘ └────┘ └┘ └┘
src ───────┘└──────┘┴ └────┘└─┘ ┴ └─┘ └───┘
typ ───────┘└──────┘┴ └────┘└─┘ ┴└┘└─┘└┘└───┘
doc ───────┘ ┴ └─┘ ┴ └─┘ └───┘
txt ───────┘ ┴ └─┘ ┴ └─┘ └───┘
par ───────┘ ┴ └─┘ ┴ └─┘ └───┘
pid ───────┘ ┴ └─┘ ┴ └─┘ └──┘┴
st ────────────────────────────────────────┘└┘└
526 { rwa abs_of_nonpos at this,
id └───────────┘
src └──┘└───────────┘└──────┘
typ └──┘└───────────┘└──────┘
doc └──┘ └──────┘
txt └──┘ └──────┘
par └──┘ └──────┘
pid ┴ └──────┘
st ────────────────────────────┘└─
527 rw abs_of_nonpos h at h₁,
id └───────────┘ ┴
src └─┘└───────────┘┴ └────┘
typ └─┘└───────────┘┴┴└────┘
doc └─┘ ┴ └────┘
txt └─┘ ┴ └────┘
par └─┘ ┴ └────┘
pid ┴ ┴ └────┘
st ───────────────────────────┘└─
528 rw [← sub_le_sub_iff_right, zero_sub],
id └──────────────────┘ └──────┘
src └────┘└──────────────────┘└┘└──────┘┴
typ └────┘└──────────────────┘└┘└──────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid └──┘ └┘ ┴
st ─────────────────────────────┘└────────┘└──
529 exact le_trans (le_of_lt (abs_lt.1 $ h₂ _ ij).2) h₁ }
id └──────┘ └──────┘ └────┘ └┘ └┘ └┘
src └────┘└──────┘┴ └──────┘┴ └────┘└─┘ ┴ └─┘ └───┘ ┴
typ └────┘└──────┘┴ └──────┘┴ └────┘└─┘ ┴└┘└─┘└┘└───┘└┘┴
doc └────┘ ┴ ┴ └─┘ ┴ └─┘ └───┘ ┴
txt └────┘ ┴ ┴ └─┘ ┴ └─┘ └───┘ ┴
par └────┘ ┴ ┴ └─┘ ┴ └─┘ └───┘ ┴
pid ┴ ┴ ┴ └─┘ ┴ └─┘ └───┘ ┴
st ───────────────────────────────────────────────────────┘└─
530 end
st ──┘
531
532 instance : has_lt (cau_seq α abs) := ⟨λ f g, pos (g - f)⟩
id └────┘ └─────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
src └────┘ └─────┘ └─┘ └─┘ ┴
typ └────┘ └─────┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─┘
533 instance : has_le (cau_seq α abs) := ⟨λ f g, f < g ∨ f ≈ g⟩
id └────┘ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ └─────┘ └─┘ ┴ ┴ ┴
typ └────┘ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
534
535 theorem lt_of_lt_of_eq {f g h : cau_seq α abs}
id └─────┘ ┴ └─┘
src └─────┘ └─┘
typ └─────┘ ┴ └─┘
536 (fg : f < g) (gh : g ≈ h) : f < h :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
537 by simpa using pos_add_lim_zero fg (neg_lim_zero gh)
id └──────────────┘ └┘ └──────────┘ └┘
src └──────────┘└──────────────┘┴ ┴ └──────────┘┴ └─
typ └──────────┘└──────────────┘┴└┘┴ └──────────┘┴└┘└─
doc └──────────┘ ┴ ┴ ┴ └─
txt └──────────┘ ┴ ┴ ┴ └─
par └──────────┘ ┴ ┴ ┴ └─
pid ┴└────┘ ┴ ┴ ┴ ┴└
st └──────────────────────────────────────────────────
538
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
539 theorem lt_of_eq_of_lt {f g h : cau_seq α abs}
id └─────┘ ┴ └─┘
src └─────┘ └─┘
typ └─────┘ ┴ └─┘
540 (fg : f ≈ g) (gh : g < h) : f < h :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
541 by have := pos_add_lim_zero gh (neg_lim_zero fg);
id └──────────────┘ └┘ └──────────┘ └┘
src └──────┘└──────────────┘┴ ┴ └──────────┘┴ ┴
typ └──────┘└──────────────┘┴└┘┴ └──────────┘┴└┘┴
doc └──────┘ ┴ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴ ┴
pid └───┘└─┘ ┴ ┴ ┴ ┴
st └───────────────────────────────────────────────
542 rwa [← sub_eq_add_neg, sub_sub_sub_cancel_right] at this
id └────────────┘ └──────────────────────┘
src └─────┘└────────────┘└┘└──────────────────────┘└─────────
typ └─────┘└────────────┘└┘└──────────────────────┘└─────────
doc └─────┘ └┘ └─────────
txt └─────┘ └┘ └─────────
par └─────┘ └┘ └─────────
pid └──┘ └┘ ┴└──────┘└
st ───────┘└──────────────┘└────────────────────────┘┴└────────
543
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
544 theorem lt_trans {f g h : cau_seq α abs} (fg : f < g) (gh : g < h) : f < h :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─┘ ┴ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
545 by simpa using add_pos fg gh
id └─────┘ └┘ └┘
src └──────────┘└─────┘┴ ┴ └
typ └──────────┘└─────┘┴└┘┴└┘└
doc └──────────┘ ┴ ┴ └
txt └──────────┘ ┴ ┴ └
par └──────────┘ ┴ ┴ └
pid ┴└────┘ ┴ ┴ └
st └──────────────────────────
546
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
547 theorem lt_irrefl {f : cau_seq α abs} : ¬ f < f
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └─────┘ └─┘ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴
548 | h := not_lim_zero_of_pos h (by simp [zero_lim_zero])
id ┴ └─────────────────┘ └───────────┘
src └─────────────────┘ └────┘└───────────┘┴
typ ┴ └─────────────────┘ └────┘└───────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────────────────┘
549
550 lemma le_of_eq_of_le {f g h : cau_seq α abs}
id └─────┘ ┴ └─┘
src └─────┘ └─┘
typ └─────┘ ┴ └─┘
551 (hfg : f ≈ g) (hgh : g ≤ h) : f ≤ h :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
552 hgh.elim (or.inl ∘ cau_seq.lt_of_eq_of_lt hfg)
id └─┘└───┘ └────┘ ┴ └────────────────────┘ └─┘
src └───┘ └────┘ ┴ └────────────────────┘
typ └─┘└───┘ └────┘ ┴ └────────────────────┘ └─┘
553 (or.inr ∘ setoid.trans hfg)
id └────┘ ┴ └──────────┘ └─┘
src └────┘ ┴ └──────────┘
typ └────┘ ┴ └──────────┘ └─┘
554
555 lemma le_of_le_of_eq {f g h : cau_seq α abs}
id └─────┘ ┴ └─┘
src └─────┘ └─┘
typ └─────┘ ┴ └─┘
556 (hfg : f ≤ g) (hgh : g ≈ h) : f ≤ h :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
557 hfg.elim (λ h, or.inl (cau_seq.lt_of_lt_of_eq h hgh))
id └─┘└───┘ ┴ └────┘ └────────────────────┘ ┴ └─┘
src └───┘ └────┘ └────────────────────┘
typ └─┘└───┘ ┴ └────┘ └────────────────────┘ ┴ └─┘
558 (λ h, or.inr (setoid.trans h hgh))
id ┴ └────┘ └──────────┘ ┴ └─┘
src └────┘ └──────────┘
typ ┴ └────┘ └──────────┘ ┴ └─┘
559
560 instance : preorder (cau_seq α abs) :=
id └──────┘ └─────┘ ┴ └─┘
src └──────┘ └─────┘ └─┘
typ └──────┘ └─────┘ ┴ └─┘
561 { lt := (<),
id ┴
src ┴
typ ┴
562 le := λ f g, f < g ∨ f ≈ g,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
563 le_refl := λ f, or.inr (setoid.refl _),
id ┴ └────┘ └─────────┘
src └────┘ └─────────┘
typ ┴ └────┘ └─────────┘
564 le_trans := λ f g h fg, match fg with
id ┴ ┴ ┴ └┘ └┘
typ ┴ ┴ ┴ └┘ └┘
565 | or.inl fg, or.inl gh := or.inl $ lt_trans fg gh
id └┘ └────┘ └┘ └────┘ └──────┘
src └────┘ └────┘ └──────┘
typ └┘ └────┘ └┘ └────┘ └──────┘
566 | or.inl fg, or.inr gh := or.inl $ lt_of_lt_of_eq fg gh
id └────┘ └┘ └────┘ └┘ └────┘ └────────────┘
src └────┘ └────┘ └────┘ └────────────┘
typ └────┘ └┘ └────┘ └┘ └────┘ └────────────┘
567 | or.inr fg, or.inl gh := or.inl $ lt_of_eq_of_lt fg gh
id └────┘ └┘ └────┘ └┘ └────┘ └────────────┘
src └────┘ └────┘ └────┘ └────────────┘
typ └────┘ └┘ └────┘ └┘ └────┘ └────────────┘
568 | or.inr fg, or.inr gh := or.inr $ setoid.trans fg gh
id └┘ └────┘ └┘ └────┘ └──────────┘
src └────┘ └────┘ └──────────┘
typ └┘ └────┘ └┘ └────┘ └──────────┘
569 end,
570 lt_iff_le_not_le := λ f g,
id ┴ ┴
typ ┴ ┴
571 ⟨λ h, ⟨or.inl h,
id ┴ └────┘ ┴
src └────┘
typ ┴ └────┘ ┴
572 not_or (mt (lt_trans h) lt_irrefl) (not_lim_zero_of_pos h)⟩,
id └────┘ └┘ └──────┘ ┴ └───────┘ └─────────────────┘ ┴
src └────┘ └┘ └──────┘ └───────┘ └─────────────────┘
typ └────┘ └┘ └──────┘ ┴ └───────┘ └─────────────────┘ ┴
573 λ ⟨h₁, h₂⟩, h₁.resolve_right
id ┴└┘ └┘ └────────────┘
src └────────────┘
typ ┴└┘ └┘ └────────────┘
574 (mt (λ h, or.inr (setoid.symm h)) h₂)⟩ }
id └┘ ┴ └────┘ └─────────┘ ┴
src └┘ └────┘ └─────────┘
typ └┘ ┴ └────┘ └─────────┘ ┴
575
576 theorem le_antisymm {f g : cau_seq α abs} (fg : f ≤ g) (gf : g ≤ f) : f ≈ g :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─┘ ┴ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
577 fg.resolve_left (not_lt_of_le gf)
id └┘└───────────┘ └──────────┘ └┘
src └───────────┘ └──────────┘
typ └┘└───────────┘ └──────────┘ └┘
578
579 theorem lt_total (f g : cau_seq α abs) : f < g ∨ f ≈ g ∨ g < f :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─┘ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
580 (trichotomy (g - f)).imp_right
id └────────┘ ┴ ┴ ┴ └───────┘
src └────────┘ ┴ └───────┘
typ └────────┘ ┴ ┴ ┴ └───────┘
581 (λ h, h.imp (λ h, setoid.symm h) (λ h, by rwa neg_sub at h))
id ┴ ┴└──┘ ┴ └─────────┘ ┴ ┴ └─────┘
src └──┘ └─────────┘ └──┘└─────┘└───┘
typ ┴ ┴└──┘ ┴ └─────────┘ ┴ ┴ └──┘└─────┘└───┘
doc └──┘ └───┘
txt └──┘ └───┘
par └──┘ └───┘
pid ┴ └───┘
st └───────────────┘
582
583 theorem le_total (f g : cau_seq α abs) : f ≤ g ∨ g ≤ f :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─┘ ┴ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
584 (or.assoc.2 (lt_total f g)).imp_right or.inl
id └──────┘┴ └──────┘ ┴ ┴ └───────┘ └────┘
src └──────┘┴ └──────┘ └───────┘ └────┘
typ └──────┘┴ └──────┘ ┴ ┴ └───────┘ └────┘
585
586 theorem const_lt {x y : α} : const x < const y ↔ x < y :=
id ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
587 show pos _ ↔ _, by rw [← const_sub, const_pos, sub_pos]
id └─┘ ┴ └───────┘ └───────┘ └─────┘
src └─┘ ┴ └────┘└───────┘└┘└───────┘└┘└─────┘└─
typ └─┘ ┴ └────┘└───────┘└┘└───────┘└┘└─────┘└─
doc └─┘ └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid └──┘ └┘ └┘ ┴└
st └──────────────┘└─────────┘└───────┘┴└
588
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
589 theorem const_le {x y : α} : const x ≤ const y ↔ x ≤ y :=
id ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ └───┘ ┴ ┴
typ ┴ └───┘ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └───┘
590 by rw le_iff_lt_or_eq; exact or_congr const_lt const_equiv
id └─────────────┘ └──────┘ └──────┘ └─────────┘
src └─┘└─────────────┘ └────┘└──────┘┴└──────┘┴└─────────┘└
typ └─┘└─────────────┘ └────┘└──────┘┴└──────┘┴└─────────┘└
doc └─┘ └────┘ ┴ ┴ └
txt └─┘ └────┘ ┴ ┴ └
par └─┘ └────┘ ┴ ┴ └
pid ┴ ┴ ┴ ┴ └
st └────────────────────────────────────────────────────────
591
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
592 lemma le_of_exists {f g : cau_seq α abs}
id └─────┘ ┴ └─┘
src └─────┘ └─┘
typ └─────┘ ┴ └─┘
593 (h : ∃ i, ∀ j ≥ i, f j ≤ g j) : f ≤ g :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
594 let ⟨i, hi⟩ := h in
id └─┘ ┴ └┘ ┴
typ └─┘ ┴ └┘ ┴
595 (or.assoc.2 (cau_seq.lt_total f g)).elim
id └──────┘┴ └──────────────┘ ┴ ┴ └──┘
src └──────┘┴ └──────────────┘ └──┘
typ └──────┘┴ └──────────────┘ ┴ ┴ └──┘
596 id
id └┘
src └┘
typ └┘
597 (λ hgf, false.elim (let ⟨K, hK0, j, hKj⟩ := hgf in
id └─┘ └────────┘ └─┘ └─┘ ┴ └─┘ └─┘
src └────────┘
typ └─┘ └────────┘ └─┘ └─┘ ┴ └─┘ └─┘
598 not_lt_of_ge (hi (max i j) (le_max_left _ _))
id └──────────┘ └─┘ └─────────┘
src └──────────┘ └─┘ └─────────┘
typ └──────────┘ └─┘ └─────────┘
599 (sub_pos.1 (lt_of_lt_of_le hK0 (hKj _ (le_max_right _ _))))))
id └─────┘┴ └────────────┘ └──────────┘
src └─────┘┴ └────────────┘ └──────────┘
typ └─────┘┴ └────────────┘ └──────────┘
600
601 theorem exists_gt (f : cau_seq α abs) : ∃ a : α, f < const a :=
id └─────┘ ┴ └─┘ ┴ ┴┴ ┴ ┴ └───┘ ┴
src └─────┘ └─┘ ┴ ┴ ┴ └───┘
typ └─────┘ ┴ └─┘ ┴ ┴┴ ┴ ┴ └───┘ ┴
doc └───┘
602 let ⟨K, H⟩ := f.bounded in
id └─┘ ┴ ┴└──────┘
src └──────┘
typ └─┘ ┴ ┴└──────┘
603 ⟨K + 1, 1, zero_lt_one, 0, λ i _, begin
id ┴ └─────────┘ ┴ ┴
src ┴ └─────────┘
typ ┴ └─────────┘ ┴ ┴
st └─────
604 rw [sub_apply, const_apply, le_sub_iff_add_le', add_le_add_iff_right],
id └───────┘ └─────────┘ └────────────────┘ └──────────────────┘
src └──┘└───────┘└┘└─────────┘└┘└────────────────┘└┘└──────────────────┘┴
typ └──┘└───────┘└┘└─────────┘└┘└────────────────┘└┘└──────────────────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st ──────────────┘└───────────┘└──────────────────┘└────────────────────┘└──
605 exact le_of_lt (abs_lt.1 (H _)).2
id └──────┘ └────┘ ┴
src └────┘└──────┘┴ └────┘└─┘ └─────┘
typ └────┘└──────┘┴ └────┘└─┘ ┴└─────┘
doc └────┘ ┴ └─┘ └─────┘
txt └────┘ ┴ └─┘ └─────┘
par └────┘ ┴ └─┘ └─────┘
pid ┴ ┴ └─┘ └──┘└─┘
st ───────────────────────────────────┘
606 end⟩
st └─┘
607
608 theorem exists_lt (f : cau_seq α abs) : ∃ a : α, const a < f :=
id └─────┘ ┴ └─┘ ┴ ┴┴ └───┘ ┴ ┴ ┴
src └─────┘ └─┘ ┴ ┴ └───┘ ┴
typ └─────┘ ┴ └─┘ ┴ ┴┴ └───┘ ┴ ┴ ┴
doc └───┘
609 let ⟨a, h⟩ := (-f).exists_gt in ⟨-a, show pos _,
id └─┘ ┴ ┴┴ └───────┘ ┴ └─┘
src ┴ └───────┘ ┴ └─┘
typ └─┘ ┴ ┴┴ └───────┘ ┴ └─┘
doc └─┘
610 by rwa [const_neg, sub_neg_eq_add, add_comm, ← sub_neg_eq_add]⟩
id └───────┘ └────────────┘ └──────┘ └────────────┘
src └───┘└───────┘└┘└────────────┘└┘└──────┘└──┘└────────────┘┴
typ └───┘└───────┘└┘└────────────┘└┘└──────┘└──┘└────────────┘┴
doc └───┘ └┘ └┘ └──┘ ┴
txt └───┘ └┘ └┘ └──┘ ┴
par └───┘ └┘ └┘ └──┘ ┴
pid └┘ └┘ └┘ └──┘ ┴
st └─────────────┘└──────────────┘└────────┘└────────────────┘┴
611
612 end abs
613
614 end cau_seq